The Coq mailing list

[Yann Zimmermann <Yann.Zimmermann AT imag.fr>]

Bonjour,

Je cherche à developper une tactique ou une commande Coq permettant :
 - la recherche de propriétés
 - la plannification de preuve
 - l'élalage de l'arbre de preuve
 - la recherche d'une ébauche de preuve (à partir d'un algotihme de
construction de modèle)

J'ai implémenté cet algorithme de construction de modèle en Caml.

Le manuel de référence de Coq n'explique pas comment construire une
tactique Coq baséee sur une implémentation en Caml.

Je cherche donc des documents et des informations expliquant comment
réaliser une commande Coq à partir d'un programme Caml.

Merci,
Yann Zimmermann