aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
Commit message (Expand)AuthorAge
* Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fixing kernel bug in typing match with let-ins in the arity.Gravatar Hugo Herbelin2015-11-22
* Pushing the backtrace in conversion anomalies.Gravatar Pierre-Marie Pédrot2015-11-09
* Conversion of polymorphic inductive types was incomplete in VM and native.Gravatar Maxime Dénès2015-10-28
* Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Hopefully clearer printing of stack when debugging evarconv unification.Gravatar Hugo Herbelin2015-08-02
* Fix incompleteness of conversion used by evarconvGravatar Matthieu Sozeau2015-06-28
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* simpl: honor Global for "simpl: never" (Close: 3206)Gravatar Enrico Tassi2015-02-27
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Fixing bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
* Fix 'don't expose cases' in cbnGravatar Pierre Boutillier2015-02-15
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Evar normalization is now done eagerly.Gravatar Pierre-Marie Pédrot2014-11-10
* Implement a different strategy to expand primitive projections only whenGravatar Matthieu Sozeau2014-10-15
* Tentative fix for a badly used Option.get in Reductionops.Gravatar Pierre-Marie Pédrot2014-10-12
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Fix the refolding by cbn of mutal constants defined in not included modulesGravatar Pierre Boutillier2014-10-01
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Fix bug #3664 by refolding projections that don't reduce in cbn.Gravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Fix bug introduced by earlier commit on first-order unification of primitiveGravatar Matthieu Sozeau2014-08-10
* - Fix handling of opaque polymorphic definitions which were turned transparent.Gravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
* Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Gravatar Matthieu Sozeau2014-07-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* - Keep all <= constraints during refinement, otherwise we might miss collapse...Gravatar Matthieu Sozeau2014-06-04
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 20:31:08 +0000