aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2011-11-16Adding postprocessing to remove "commutative cuts" expansions inherbelin
2011-11-16Changed the way find_dependencies_signature is working so that itherbelin
2011-11-16De Bruijn indices bug in pattern matching compilation in the presenceherbelin
2011-11-16Old generalization bug in pattern-matching: names were considered theherbelin
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
2011-11-16Old typing bug in pattern-matching compilation (apparently w/oherbelin
2011-11-16Specialization of tomatch in pattern-matching compilation was done tooherbelin
2011-11-16A bit of documentation around cases.ml + ML modules uselessly openherbelin
2011-11-16Fixing dependencies lifting bug in pattern-matching compilationherbelin
2011-11-08Refined second_order_matching so that a constraint on whichherbelin
2011-11-08optimization: memoization for is_open_canonical_projectiongareuselesinge
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-26Deactivating second-order pattern-matching in evarconv for 8.4.herbelin
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 09:35:42 +0000