| Age | Commit message (Expand) | Author |
|---|
| 2020-07-09 | [error handling] Anomaly in Conversion is a "precatchable_exception" | Emilio Jesus Gallego Arias |
| 2019-12-22 | Rename files with Class in their name to make their role clearer. | Pierre-Marie Pédrot |
| 2019-09-25 | Move cumulativity inference to the kernel. | Pierre-Marie Pédrot |
| 2019-08-18 | [api] Move `Keys` to pretyping | Emilio Jesus Gallego Arias |
| 2019-03-14 | Add relevance marks on binders. | Gaëtan Gilbert |
| 2018-09-10 | Moving part of pretyping dealing with ltac and renaming in new module GlobEnv. | Hugo Herbelin |
| 2018-07-24 | Move Heads to pretyping (is_projection will move to Recordops) | Gaëtan Gilbert |
| 2018-05-31 | [api] Move `Constrexpr` to the `interp` module. | Emilio Jesus Gallego Arias |
| 2018-05-23 | [api] Move `Vernacexpr` to parsing. | Emilio Jesus Gallego Arias |
| 2018-04-23 | [api] Relocate `intf` modules according to dependency-order. | Emilio Jesus Gallego Arias |
| 2018-02-11 | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert |
| 2017-11-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias |
| 2017-10-25 | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias |
| 2017-09-19 | Allow declaring universe constraints at definition level. | Matthieu Sozeau |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot |
| 2016-03-20 | Making Evarutil independent from Reductionops. | Pierre-Marie Pédrot |
| 2016-03-20 | Splitting Evarutil in two distinct files. | Pierre-Marie Pédrot |
| 2016-03-20 | Pushing Proofview further down the dependency alley. | Pierre-Marie Pédrot |
| 2016-03-20 | Moving Proofview to pretyping/. | Pierre-Marie Pédrot |
| 2015-07-06 | Merge branch 'v8.5' into trunk | Maxime Dénès |
| 2015-07-05 | Fix handling of primitive projections in VM. | Maxime Dénès |
| 2015-02-27 | Adding a new folder corresponding to the low-level part of the pretyper | Pierre-Marie Pédrot |
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin |
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin |
| 2014-11-26 | Experimenting always forcing convertibility on strict implicit arguments | Hugo Herbelin |
| 2014-10-01 | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot |
| 2014-03-02 | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey |
| 2013-02-10 | Splitted Evarutil in two files | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-08-24 | correct some ends of .mllib files (avoid a broken tolink.ml) | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2011-11-21 | Renamig support added to "Arguments" | gareuselesinge |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-04-05 | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin |
| 2009-12-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-03-20 | Many changes in the Makefile infrastructure + a beginning of ocamlbuild | letouzey |
