aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2011-10-17Partly reverting r14539 about fully expanding "let-in"s and not justherbelin
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-10-11Unification in the return clause of match was not supported in solve_evars.herbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
2011-10-10Fixing buggy abberant code for Evarutil.expand_evarherbelin
2011-10-10Little code simplification of instantiate_evar in evd.mlherbelin
2011-10-10Added information about evar origin in pretty-printing evd for debugherbelin
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
2011-09-26Adding subst_term up to convherbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-08Two bugs in pattern-matching compilation:herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-01 20:58:03 +0000