| Commit message (Expand) | Author | Age |
* | Removing the old implementation of clear_body. | Pierre-Marie Pédrot | 2014-09-05 |
* | 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-09-04 |
* | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau | 2014-08-22 |
* | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
* | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | 2014-08-05 |
* | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin | 2014-06-13 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
* | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin | 2014-06-01 |
* | - 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-05-06 |
* | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
* | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot | 2014-03-31 |
* | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | 2014-03-05 |
* | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey | 2014-03-02 |
* | Code refactoring thanks to the new Monad module. | Arnaud Spiwack | 2014-02-27 |
* | More sharing in Logic, together with some code cleaning. | Pierre-Marie Pédrot | 2014-02-21 |
* | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot | 2014-02-03 |
* | Algebraized "No such hypothesis" errors | Pierre-Marie Pédrot | 2014-01-06 |
* | Useless array to list conversions in proof/logic.ml. | ppedrot | 2013-10-28 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey | 2013-10-23 |
* | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | Replacing lists by sets in clear tactic. | ppedrot | 2013-08-25 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Getting rid of LtacLocated exception transformer. | ppedrot | 2013-05-28 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Fixing #2968. This is quite brittle though, because we are messing | ppedrot | 2013-04-16 |
* | Allow catching of WrongAbstractionType, fixing a regression from 8.4 | msozeau | 2013-04-05 |
* | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey | 2013-03-13 |
* | Removing Exc_located and using the new exception enrichement | ppedrot | 2013-02-18 |
* | 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-02-17 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Renamed Option.Misc.compare to the more uniform Option.equal. | ppedrot | 2012-12-13 |
* | Monomorphization (proof) | ppedrot | 2012-11-25 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | 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-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Glob_term now mli-only, operations now in Glob_ops | letouzey | 2012-05-29 |