aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
Commit message (Expand)AuthorAge
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Making Evd independent from Namegen.Gravatar Pierre-Marie Pédrot2017-02-14
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|/|
| * Document changesGravatar Matthieu Sozeau2016-12-02
| * Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
* | Reordering Termops w.r.t. Evd and Namegen in engine folder.Gravatar Pierre-Marie Pédrot2016-10-30
|/
* Short documentation, filling TODO's in evd.mli.Gravatar Hugo Herbelin2016-09-01
* Remove unused optional "predicative" argument.Gravatar Guillaume Melquiond2016-08-10
* Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
* mergeGravatar Matej Kosik2016-01-11
|\
| * CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-01
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
* Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
* Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
* Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
* Removing meta_with_name from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* Removing subst_defined_metas_evars from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27