aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.mli
Commit message (Expand)AuthorAge
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* State Transaction MachineGravatar gareuselesinge2013-08-08
* raise UnsafeSuccess -> feedback AddedAxiomGravatar gareuselesinge2013-04-25
* Updating headers.Gravatar herbelin2012-08-08
* Vecnacentries.dump_global silently ignores exceptionsGravatar pboutill2012-08-06
* A new status Unsafe in Interface. Meant for commands such as Admitted.Gravatar aspiwack2012-07-12
* Getting rid of Pcoq remains.Gravatar ppedrot2012-06-12
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* correct abort in Function when a proof of inversion failsGravatar letouzey2012-04-23
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Noise for nothingGravatar pboutill2012-03-02
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Coqide: new backtracking code, based on the Backtrack commandGravatar letouzey2011-09-05
* Misc improvements concerning "Show Match" and its coqide equivalentGravatar letouzey2011-08-18
* New option [Set Bullet Behavior] allows to select the behaviour of bullets.Gravatar aspiwack2011-05-13
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-05-03
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Nouvelle en-têteGravatar herbelin2004-07-16
* Deplacement pr_subgoal and co vers PfeditGravatar herbelin2003-10-13
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* export a function that is needed in pcoq.Gravatar bertot2001-02-13
* exported several functions that are used in the graphical interface pcoq.Gravatar bertot2001-02-09
* export a function that can be used to retrieve the context correspondingGravatar bertot2001-02-08
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* documentation interfacesGravatar filliatr1999-12-13
* module MetasyntaxGravatar filliatr1999-12-01
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24