aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
AgeCommit message (Expand)Author
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Matthieu Sozeau
2014-06-25Use full transparent state when checking well-typedness of a second order mat...Matthieu Sozeau
2014-06-17Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
2014-06-13Adapt simpl/cbn unfolding and refolding machinery to projections, so thatMatthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-08Fix canonical structure resolution in unification (bug found in Ssreflect).Matthieu Sozeau
2014-06-04Fix canonical structure resolution (makes test-suite files go through again).Matthieu Sozeau
2014-05-16More fixes of unification with primitive projections (missed cases during the...Matthieu Sozeau
2014-05-16Fix unification of non-unfoldable primitive projections in evarconv.Matthieu Sozeau
2014-05-09Fix second-order matching to properly check that the predicate found byMatthieu Sozeau
2014-05-06- Add back some compatibility functions to avoid rewriting plugins.Matthieu Sozeau
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06In case two constants/vars/rels are _not_ defined, force unification of unive...Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-01Propagating conversion_problem towards (postponed) evar/evar problems.Hugo Herbelin
2014-03-17Evarconv: exact_ise_stack looks to stack head before bodies or branchesPierre Boutillier
2014-03-16consider_remaining_unif_problems respects Conv_oraclePierre Boutillier
2014-03-10Evarconv unification respects Conv_oraclePierre Boutillier
2014-03-10MaybeFlexible semantic changesPierre Boutillier
2014-02-24Create Debug Unification optionPierre Boutillier
2014-02-24No more translation array <-> list in Reductionops.StackPierre Boutillier
2014-02-24Reductionops.Stack.strip* are ready to deal with ShiftPierre Boutillier
2014-02-24Reductionops.Stack.app_node is secretPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-23Small optimizations in unification.ppedrot
2013-10-22Removing useless array-to-list and converse casts used inppedrot
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-05-30Do not compute fallback eagerly in Evarconvpboutill
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-06Small cleaning of Evd interface.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-17Fix of r16257 in r16205 for "errors raised by check_evar_instance wereherbelin
2013-04-17Like in r16346, do not filter local definitions (here in theherbelin
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
2013-03-25Fix bug #2989: make unification.ml able to deal with canonical structure in a...pboutill
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-03-05More monomorphization.ppedrot
2013-02-28compare_stack_shape before ise_stack2 in evar_convpboutill
2013-02-28Repairing r16205: errors raised by check_evar_instance were no longerherbelin
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...pboutill
2013-02-17A more informative message when the elimination predicate forherbelin
2013-02-17Locating errors from consider_remaining_unif_problems if possibleherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 05:52:54 +0000