| Age | Commit message (Expand) | Author |
|---|
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot |
| 2014-06-24 | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-22 | Removing the compatibility layer from Leminv. Also removed an undocumented | Pierre-Marie Pédrot |
| 2014-03-28 | Define Tactics.bring_hyps in the new monad. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 2013-11-04 | Allowing proofs starting with a non-empty evarmap. | ppedrot |
| 2013-11-02 | Tachmach.New is now in Proofview.Goal.enter style. | aspiwack |
| 2013-11-02 | More Proofview.Goal.enter. | aspiwack |
| 2013-11-02 | The tactic [admit] exits with the "unsafe" status. | aspiwack |
| 2013-11-02 | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-13 | Fixed bug #2314 (inversion using not checking the correctness of its arguments | herbelin |
| 2010-05-26 | Fixing Derive Inversion for new proof engine | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2009-02-06 | pushed evar reduction in kernel | barras |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
