aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
* Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
* 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
|\
* | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-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
* mergeGravatar Matej Kosik2016-01-11
|\
| * CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-01
* | 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
* API: documenting context_chop and removing a duplicate.Gravatar Hugo Herbelin2015-12-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
* Fixing compilation of mli documentation.Gravatar Hugo Herbelin2015-12-05
* Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* 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-26
* More invariants in UState.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
* Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
* Removing some unsafe uses of monotonicity.Gravatar Pierre-Marie Pédrot2015-10-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
* Adding a notion of monotonous evarmap.Gravatar Pierre-Marie Pédrot2015-10-18
* 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
* 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
* Fix documentation.Gravatar Matthieu Sozeau2015-07-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 01:51:57 +0000