aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
Commit message (Expand)AuthorAge
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
| * Remove TODO comment (Evar.t is opaque)Gravatar Gaëtan Gilbert2017-09-29
* | Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
|/
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| |\
| * | Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
| | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |/
* | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* | [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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 04:18:33 +0000