aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Tentative fix for a badly used Option.get in Reductionops.Gravatar Pierre-Marie Pédrot2014-10-12
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Do not expand primitive projections eagerly in evarconv, but onlyGravatar Matthieu Sozeau2014-10-10
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
* Add a "Debug Tactic Unification" option and correct the first-orderGravatar Matthieu Sozeau2014-10-10
* Make constrMatching and detyping more robust with respect toGravatar Matthieu Sozeau2014-10-10
* Fix bug due to shadowing a variable name in tacredGravatar Matthieu Sozeau2014-10-10
* fix make mlidocGravatar Pierre Boutillier2014-10-08
* Fixing the anomaly in bug #3045 (a filter was not type-safe inGravatar Hugo Herbelin2014-10-08
* Build unfolded versions of the primitive projection in let (a, p) := ...Gravatar Matthieu Sozeau2014-10-07
* Avoid a warning with Meta's names in debugger.Gravatar Hugo Herbelin2014-10-07
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Fixing ennoying warning about evars named ?23 and so on.Gravatar Hugo Herbelin2014-10-03
* Fixing #3623 (unbound evars in types in a call to "change with").Gravatar Hugo Herbelin2014-10-03
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
* Completing fixing order of parameters when translating fromGravatar Hugo Herbelin2014-10-02
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Fix the refolding by cbn of mutal constants defined in not included modulesGravatar Pierre Boutillier2014-10-01
* Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsGravatar Hugo Herbelin2014-10-01
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
* Fix bug #3664 by refolding projections that don't reduce in cbn.Gravatar Matthieu Sozeau2014-09-27
* Fix semantics of matching with folded/unfolded projections to definitelyGravatar Matthieu Sozeau2014-09-27
* Fix bug #3672, application of primitive projections as coercions.Gravatar Matthieu Sozeau2014-09-27
* Fix bug 3662 by actually reducing primitive projections in cbv/compute.Gravatar Matthieu Sozeau2014-09-27
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix canonical structure resolution which was launched on the results ofGravatar Matthieu Sozeau2014-09-26
* Fix incorrect assert false in detyping.Gravatar Matthieu Sozeau2014-09-25
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Return a Prop not an arbitrary Type, and correct a typo.Gravatar Matthieu Sozeau2014-09-24
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Fix bug #3656.Gravatar Matthieu Sozeau2014-09-23
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fixes in Ltac pattern-matching on primitive projectionsGravatar Matthieu Sozeau2014-09-19
* Use smart mapping in map_constr_with_binders_left_to_right.Gravatar Matthieu Sozeau2014-09-19
* Fixing #3641 (loop in e_contextually, introduced in r16525).Gravatar Hugo Herbelin2014-09-19
* Revert change of e_contextually as it needlessly expands all primitiveGravatar Matthieu Sozeau2014-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:46:08 +0000