aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
AgeCommit message (Expand)Author
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
2013-02-10Splitted Evarutil in two filesppedrot
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22- Fix evarconv so that we have complete eta-conversion:msozeau
2013-01-18Evarconv: Check stack before term in Canonical Structure approuvalpboutill
2012-12-19Reductionops reduction machine can refold constantpboutill
2012-12-19Evarconv.Pseudorigid erasurepboutill
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-28Evarconv: Fix #2936 + commentspboutill
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-20Cleaning and small optimization in CList.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 11:43:02 +0000