aboutsummaryrefslogtreecommitdiff
path: root/tactics/refine.mli
AgeCommit message (Expand)Author
2013-11-02A whole new implemenation of the refine tactic.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2012-08-08Updating headers.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-07-16Nouvelle en-têteherbelin
2003-12-13Correction bug soumis par Yvesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...herbelin
2000-07-20portage Refinefilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:52:09 +0000