aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mllib
Commit message (Expand)AuthorAge
* [api] Move `Constrexpr` to the `interp` module.Gravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
* Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* Pushing Proofview further down the dependency alley.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Proofview to pretyping/.Gravatar Pierre-Marie Pédrot2016-03-20
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-06
|\
| * Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* | Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
|/
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20