aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-08-03Fix nf_evars_undefinedmsozeau
2011-08-02Patch to simplify is_open_canonical_projectionherbelin
2011-08-02More robust evar_map debugging printerherbelin
2011-07-29Evarutil: replace generic list_distinct on constr by constr_list_distinctpuech
2011-07-29Evarutil: replaced some generic = on constr by destructorspuech
2011-07-29Evarutil: generic equality on constr replaced by destructorspuech
2011-07-29Evarconv: generic equality on constr replaced by eq_constrpuech
2011-07-29Cases: generic equality on constr replaced by destructorspuech
2011-07-29Classops: generic equality on constr replaced by eq_constrpuech
2011-07-29Evarutil: generic equality on constr replaced by eq_constr (x2)puech
2011-07-29Evarutil: generic equality on constr replaced by eq_constrpuech
2011-07-29Tacred: generic equality on constr replaced by eq_constrpuech
2011-07-16This is exactly the structure needed to handle controlling printingherbelin
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-20Fixing two typos introduced in r14217 and r14223herbelin
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-18Activating flags betaiota by default for applyherbelin
2011-06-18The ad hoc version for first-order unification at toplevel of "?n argsherbelin
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Oups, typo in previous commitherbelin
2011-06-12Removed what looks like a (very old) useless f.o. unification passherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing constrai...msozeau
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
2011-06-08Fixes in pruning in unification.msozeau
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to typechec...msozeau
2011-05-24Applying Enrico Tassi's patch for giving priority to delta over eta inherbelin
2011-05-15Failing instead of switching to the coercion mechanism when VMcastherbelin
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
2011-05-05Fix merge, Cumul moved to CUMULmsozeau
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-04-24Fixing bug in printing let-in binders in fix/cofixherbelin
2011-04-20Allow betaiota when checking unification of the types of metas (fixes ATBR co...msozeau
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-04-16Fix unification of types of metavariables and error message for sort unificat...msozeau
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
2011-04-13- Make typeclass transparency information directly availablemsozeau
2011-04-13- Remove create_evar_defsmsozeau
2011-04-13- Improve unification (beta-reduction, and same heuristic as evarconv for red...msozeau
2011-04-13Unify meta types with the right flags, add betaiotazeta reduction to unificat...msozeau
2011-04-13Proper typing of metavariables, type errors were completely ignored before......msozeau
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
2011-04-11Catch NotArity exception and transform it into an anomaly in retyping.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 11:20:33 +0000