aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Expand)Author
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
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-18Reductionops: (Co)Fixpoints are always refolded during iotaPierre Boutillier
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-06Cleanup code for looking up projection bodies.Matthieu Sozeau
2014-08-26Debug RAKAMPierre Boutillier
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-10Fix bug introduced by earlier commit on first-order unification of primitiveMatthieu Sozeau
2014-08-03- Fix handling of opaque polymorphic definitions which were turned transparent.Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-29Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsMatthieu Sozeau
2014-07-10Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 10:57:38 +0000