aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
...
* Fix for subclasses implementation, allowing to register generalized classes s...Gravatar msozeau2011-11-18
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Adding postprocessing to remove "commutative cuts" expansions inGravatar herbelin2011-11-16
* Changed the way find_dependencies_signature is working so that itGravatar herbelin2011-11-16
* De Bruijn indices bug in pattern matching compilation in the presenceGravatar herbelin2011-11-16
* Old generalization bug in pattern-matching: names were considered theGravatar herbelin2011-11-16
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Old typing bug in pattern-matching compilation (apparently w/oGravatar herbelin2011-11-16
* Specialization of tomatch in pattern-matching compilation was done tooGravatar herbelin2011-11-16
* A bit of documentation around cases.ml + ML modules uselessly openGravatar herbelin2011-11-16
* Fixing dependencies lifting bug in pattern-matching compilationGravatar herbelin2011-11-16
* Refined second_order_matching so that a constraint on whichGravatar herbelin2011-11-08
* optimization: memoization for is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Deactivating second-order pattern-matching in evarconv for 8.4.Gravatar herbelin2011-10-26
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
* Fixing use of type constraint for refining the "return" clause of "match".Gravatar herbelin2011-10-25
* Continuing r14585 (ill-typed restriction bug).Gravatar herbelin2011-10-25
* Continuing r1492 (useless changes were inadvertantly committed)Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* Still more unification in typing.mlGravatar herbelin2011-10-25
* More unification in type_of and addition of e_type_of to get the newGravatar herbelin2011-10-24
* Fixing another bug revealing ill-typed use of evar restriction.Gravatar herbelin2011-10-24
* Fixing instance/filter mismatch in materialize_evar + documentation.Gravatar herbelin2011-10-24
* Fail if some conv pbs remain after consider_remaining_unif_problems.Gravatar herbelin2011-10-22
* Now consider remaining conversion problems in solve_remaining_evars.Gravatar herbelin2011-10-22
* Use also second-order unification if first-order fails at the time of conside...Gravatar herbelin2011-10-22
* Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...Gravatar herbelin2011-10-22
* Partly reverting r14539 about fully expanding "let-in"s and not justGravatar herbelin2011-10-17
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
* Unification in the return clause of match was not supported in solve_evars.Gravatar herbelin2011-10-11
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* More robust and uniform treatment of aliases in evarutil.mlGravatar herbelin2011-10-10
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
* Fixing buggy abberant code for Evarutil.expand_evarGravatar herbelin2011-10-10
* Little code simplification of instantiate_evar in evd.mlGravatar herbelin2011-10-10
* Added information about evar origin in pretty-printing evd for debugGravatar herbelin2011-10-10
* Passed conv_algo to evar_define and move call to solve_refl toGravatar herbelin2011-10-10
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
* Adding subst_term up to convGravatar herbelin2011-09-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 01:14:21 +0000