aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* Use full transparent state when checking well-typedness of a second order mat...Gravatar Matthieu Sozeau2014-06-25
* Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Gravatar Matthieu Sozeau2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Fix canonical structure resolution in unification (bug found in Ssreflect).Gravatar Matthieu Sozeau2014-06-08
* Fix canonical structure resolution (makes test-suite files go through again).Gravatar Matthieu Sozeau2014-06-04
* More fixes of unification with primitive projections (missed cases during the...Gravatar Matthieu Sozeau2014-05-16
* Fix unification of non-unfoldable primitive projections in evarconv.Gravatar Matthieu Sozeau2014-05-16
* Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
* - Add back some compatibility functions to avoid rewriting plugins.Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* In case two constants/vars/rels are _not_ defined, force unification of unive...Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Propagating conversion_problem towards (postponed) evar/evar problems.Gravatar Hugo Herbelin2014-04-01
* Evarconv: exact_ise_stack looks to stack head before bodies or branchesGravatar Pierre Boutillier2014-03-17
* consider_remaining_unif_problems respects Conv_oracleGravatar Pierre Boutillier2014-03-16
* Evarconv unification respects Conv_oracleGravatar Pierre Boutillier2014-03-10
* MaybeFlexible semantic changesGravatar Pierre Boutillier2014-03-10
* Create Debug Unification optionGravatar Pierre Boutillier2014-02-24
* No more translation array <-> list in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.app_node is secretGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* Small optimizations in unification.Gravatar ppedrot2013-10-23
* Removing useless array-to-list and converse casts used inGravatar ppedrot2013-10-22
* Optimizing evar filters. It seems to cost quite a lot in unification,Gravatar ppedrot2013-10-22
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Do not compute fallback eagerly in EvarconvGravatar pboutill2013-05-30
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Small cleaning of Evd interface.Gravatar ppedrot2013-05-06
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Fix of r16257 in r16205 for "errors raised by check_evar_instance wereGravatar herbelin2013-04-17
* Like in r16346, do not filter local definitions (here in theGravatar herbelin2013-04-17
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
* Fix bug #2989: make unification.ml able to deal with canonical structure in a...Gravatar pboutill2013-03-25
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* More monomorphization.Gravatar ppedrot2013-03-05
* compare_stack_shape before ise_stack2 in evar_convGravatar pboutill2013-02-28
* Repairing r16205: errors raised by check_evar_instance were no longerGravatar herbelin2013-02-28
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
* Locating errors from consider_remaining_unif_problems if possibleGravatar herbelin2013-02-17
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 15:49:48 +0000