aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2011-10-25Fixing use of type constraint for refining the "return" clause of "match".herbelin
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
2011-10-25Continuing r1492 (useless changes were inadvertantly committed)herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-25Still more unification in typing.mlherbelin
2011-10-24More unification in type_of and addition of e_type_of to get the newherbelin
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
2011-10-22Fail if some conv pbs remain after consider_remaining_unif_problems.herbelin
2011-10-22Now consider remaining conversion problems in solve_remaining_evars.herbelin
2011-10-22Use also second-order unification if first-order fails at the time of conside...herbelin
2011-10-22Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 22:37:51 +0000