aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Expand)Author
2016-11-30Univs: fix bug #5180Matthieu Sozeau
2016-09-28Remove incorrect assertion in cbn (bug #4822).Guillaume Melquiond
2016-09-09no-refold patchPaul Steckler
2016-08-19[pp] Fix newline issues.Emilio Jesus Gallego Arias
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-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-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-02Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Guillaume Melquiond
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reductionops moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-15Avoid dependency of the pretyper on C code.Maxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Hopefully clearer printing of stack when debugging evarconv unification.Hugo Herbelin
2015-06-28Fix incompleteness of conversion used by evarconvMatthieu Sozeau
2015-03-04Fix bug #3532, providing universe inconsistency information when aMatthieu Sozeau
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
2015-02-27simpl: honor Global for "simpl: never" (Close: 3206)Enrico Tassi
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-21Fixing bug #3071.Pierre-Marie Pédrot
2015-02-15Fix 'don't expose cases' in cbnPierre Boutillier
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-11-10Evar normalization is now done eagerly.Pierre-Marie Pédrot
2014-10-15Implement a different strategy to expand primitive projections only whenMatthieu Sozeau
2014-10-12Tentative fix for a badly used Option.get in Reductionops.Pierre-Marie Pédrot
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-10-02Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Matthieu Sozeau
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
2014-10-01Fix the refolding by cbn of mutal constants defined in not included modulesPierre Boutillier
2014-09-30Simplify evarconv thanks to new delta status of projections,Matthieu Sozeau
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-27Fix bug #3664 by refolding projections that don't reduce in cbn.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 19:30:33 +0000