aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
Commit message (Expand)AuthorAge
...
* | | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\|
| | * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| * | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|/| | | |/
| * 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
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...Gravatar Matej Kosik2016-08-26
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionGravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Two protections against failures when printing evar_map.Gravatar Hugo Herbelin2016-08-17
* Remove unused optional "predicative" argument.Gravatar Guillaume Melquiond2016-08-10
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
| * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
* Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
* CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
* More efficient implementation of equality-up-to-universes in Universes.Gravatar Pierre-Marie Pédrot2015-11-26
* 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-15
* 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-06
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
* 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