aboutsummaryrefslogtreecommitdiff
path: root/tactics/extratactics.mli
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2012-12-14Modulification of identifierppedrot
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
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
2009-12-21Generic support for open terms in tacticsherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-06-23Correction ident -> hyp pour dinterpréter des identificateurs devant êt...herbelin
2006-05-02Extension syntaxique de rewrite in: au lieu de pouvoir faire letouzey
2006-03-21+ destruct now works as induction on multiple arguments : jforest
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-16Nouvelle en-têteherbelin
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...herbelin
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin