| Age | Commit message (Expand) | Author |
|---|
| 2014-10-04 | A few Global.env removed. | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-05 | Removing the old implementation of clear_body. | Pierre-Marie Pédrot |
| 2014-09-04 | Revert the two previous commits. I was testing in the wrong branch. | Pierre-Marie Pédrot |
| 2014-09-04 | Removing the old implementation of clear_body. | Pierre-Marie Pédrot |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin |
| 2014-06-13 | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-06-01 | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | 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-03-31 | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey |
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack |
| 2014-02-21 | More sharing in Logic, together with some code cleaning. | Pierre-Marie Pédrot |
| 2014-02-03 | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot |
| 2014-01-06 | Algebraized "No such hypothesis" errors | Pierre-Marie Pédrot |
| 2013-10-28 | Useless array to list conversions in proof/logic.ml. | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-08-25 | Replacing lists by sets in clear tactic. | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-28 | Getting rid of LtacLocated exception transformer. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-16 | Fixing #2968. This is quite brittle though, because we are messing | ppedrot |
| 2013-04-05 | Allow catching of WrongAbstractionType, fixing a regression from 8.4 | msozeau |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey |
| 2013-02-18 | Removing Exc_located and using the new exception enrichement | ppedrot |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-02-17 | Revised the Ltac trace mechanism so that trace breaking due to | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-13 | Renamed Option.Misc.compare to the more uniform Option.equal. | ppedrot |
| 2012-11-25 | Monomorphization (proof) | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | 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-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
