aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Make semantics of whd_zeta consistent with other whd_* functions.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29Program: cleanup in cases, add optionsMatthieu Sozeau
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Rework treatment of default transparency of obligationsMatthieu Sozeau
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-27More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Hugo Herbelin
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Typeclasses:rename solve_instantiation* & use HookMatthieu Sozeau
2016-06-16Refine 9cc95f5, unification of Let-In's, bug #3929Matthieu Sozeau
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-15Allow `Pretyping.search_guard` to not check guardArnaud Spiwack
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
2016-06-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-13evar_conv: Refine occur_rigidlyMatthieu Sozeau
2016-06-12Minor simplification in evarconv.Hugo Herbelin
2016-06-12Reserve exception "ConversionFailed" in unification for failure ofHugo Herbelin
2016-06-12Protecting eta-expansion in evarconv.ml against ill-typed problems.Hugo Herbelin
2016-06-10A mini-optimization for free in unification.ml: test in O(1)Hugo Herbelin
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-09Fixing #4644 (regression of unification on evar-evar problems with a match).Hugo Herbelin
2016-06-09Minor simplification in evarconv.ml.Hugo Herbelin
2016-06-09Reverting dbdff037 which does not seem to prevent to have #3638 fixedHugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-13More informative error message when interpreting ltac variables in terms.Pierre-Marie Pédrot
2016-05-12Small optimization in evar resolution.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Use the canonical name when looking for an eliminator (bug #4670).Guillaume Melquiond
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
2016-04-27Revert "More abstraction in cases.mli."Hugo Herbelin
2016-04-27Revert "Add support for generalization also on named variables in pattern-mat...Hugo Herbelin
2016-04-27Revert "Add support for deep dependencies in variables within the recursive s...Hugo Herbelin
2016-04-27Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Hugo Herbelin
2016-04-27Revert "Using existing names as a basis for the inner names of the pattern-ma...Hugo Herbelin
2016-04-27Revert "Vers un filtrage profond ..."Hugo Herbelin
2016-04-27Vers un filtrage profond ...Hugo Herbelin
2016-04-27Using existing names as a basis for the inner names of the pattern-matching p...Hugo Herbelin
2016-04-27Fixing a De Bruijn bug in computing return predicate by inversion.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:54:56 +0000