| Age | Commit message (Expand) | Author |
|---|
| 2017-02-15 | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias |
| 2016-09-08 | Unplugging Tacexpr in several interface files. | Pierre-Marie Pédrot |
| 2016-03-20 | Moving Tacinterp to Hightactics. | Pierre-Marie Pédrot |
| 2016-03-19 | Moving VernacSolve to an EXTEND-based definition. | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-09-25 | The -require option now accepts a logical path instead of a physical one. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-04-25 | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-04-25 | raise UnsafeSuccess -> feedback AddedAxiom | gareuselesinge |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-06 | Vecnacentries.dump_global silently ignores exceptions | pboutill |
| 2012-07-12 | A new status Unsafe in Interface. Meant for commands such as Admitted. | aspiwack |
| 2012-06-12 | Getting rid of Pcoq remains. | ppedrot |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-04-23 | correct abort in Function when a proof of inversion fails | letouzey |
| 2012-03-23 | A unified backtrack mechanism, with a basic "Show Script" as side-effect | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-09-12 | Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the... | aspiwack |
| 2011-09-05 | Coqide: new backtracking code, based on the Backtrack command | letouzey |
| 2011-08-18 | Misc improvements concerning "Show Match" and its coqide equivalent | letouzey |
| 2011-05-13 | New option [Set Bullet Behavior] allows to select the behaviour of bullets. | aspiwack |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2008-02-22 | Merge with lmamane's private branch: | lmamane |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2006-05-03 | Cleanning and factorizing code in funind. Spliting new_arg_principles into to... | jforest |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-10-13 | Deplacement pr_subgoal and co vers Pfedit | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2001-11-06 | Suite de la suppression : enamed_declaration est remplace par evar_map. | clrenard |
| 2001-10-11 | Suppression option immediate_discharge; nettoyage de Declare et conséquences | herbelin |
| 2001-03-15 | entetes | filliatr |
| 2001-03-01 | Déplacement de qualid dans Nametab, hors du noyau | herbelin |
| 2001-02-13 | export a function that is needed in pcoq. | bertot |
| 2001-02-09 | exported several functions that are used in the graphical interface pcoq. | bertot |
| 2001-02-08 | export a function that can be used to retrieve the context corresponding | bertot |
| 2000-12-12 | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr |
| 2000-09-10 | Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract... | herbelin |
