aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-15API: documenting context_chop and removing a duplicate.Hugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-05Fixing compilation of mli documentation.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05About building of substitutions from instances.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-01Remove unneeded fixpoint in normalize_context_set. Note that it is noMatthieu Sozeau
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-26More invariants in UState.Pierre-Marie Pédrot
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Removing some unsafe uses of monotonicity.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-27Removing meta_with_name from Evd.Pierre-Marie Pédrot
2015-09-27Removing subst_defined_metas_evars from Evd.Pierre-Marie Pédrot
2015-09-27Removing uselessly duplicated function in Evd.Pierre-Marie Pédrot
2015-09-26Hardening the API of evarmaps.Pierre-Marie Pédrot
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-27Fix documentation.Matthieu Sozeau
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-07Adding a primitive to the tactic monad to modify the exceptional content.Pierre-Marie Pédrot
2015-05-06Exposing the minimal amount of internal of the Logic monad in order toPierre-Marie Pédrot
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-28Moving Proofview_monad to the engine/ folder.Pierre-Marie Pédrot
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:47:53 +0000