aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2014-10-13Moving function about locs in locusops.Hugo Herbelin
2014-10-13English typo in a function name of evarconv.Hugo Herbelin
2014-10-13Added support for several impossible cases in compilation of "match".Hugo Herbelin
2014-10-12Tentative fix for a badly used Option.get in Reductionops.Pierre-Marie Pédrot
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Do not expand primitive projections eagerly in evarconv, but onlyMatthieu Sozeau
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-10Add a "Debug Tactic Unification" option and correct the first-orderMatthieu Sozeau
2014-10-10Make constrMatching and detyping more robust with respect toMatthieu Sozeau
2014-10-10Fix bug due to shadowing a variable name in tacredMatthieu Sozeau
2014-10-08fix make mlidocPierre Boutillier
2014-10-08Fixing the anomaly in bug #3045 (a filter was not type-safe inHugo Herbelin
2014-10-07Build unfolded versions of the primitive projection in let (a, p) := ...Matthieu Sozeau
2014-10-07Avoid a warning with Meta's names in debugger.Hugo Herbelin
2014-10-05A few improvements on pattern-matching compilation.Hugo Herbelin
2014-10-04A few Global.env removed.Hugo Herbelin
2014-10-03Fixing ennoying warning about evars named ?23 and so on.Hugo Herbelin
2014-10-03Fixing #3623 (unbound evars in types in a call to "change with").Hugo Herbelin
2014-10-03Fixing #3634 (wrong env in "cannot instantiate because not in itsHugo Herbelin
2014-10-02Fixing interpretation of constr under binders which was broken afterHugo Herbelin
2014-10-02Completing fixing order of parameters when translating fromHugo Herbelin
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-10-02Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Matthieu Sozeau
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
2014-10-01Fix the refolding by cbn of mutal constants defined in not included modulesPierre Boutillier
2014-10-01Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsHugo Herbelin
2014-10-01Fixing use of arguments renaming in apply which was broken afterHugo Herbelin
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-30Simplify evarconv thanks to new delta status of projections,Matthieu Sozeau
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-29Restoring non-uniform delta on local and global constants in 2nd orderHugo Herbelin
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Index keys instead of simply global references.Matthieu Sozeau
2014-09-27First version of keyed subterm selection in unification.Matthieu Sozeau
2014-09-27Fix bug #3664 by refolding projections that don't reduce in cbn.Matthieu Sozeau
2014-09-27Fix semantics of matching with folded/unfolded projections to definitelyMatthieu Sozeau
2014-09-27Fix bug #3672, application of primitive projections as coercions.Matthieu Sozeau
2014-09-27Fix bug 3662 by actually reducing primitive projections in cbv/compute.Matthieu Sozeau
2014-09-27Make pattern_of_constr typed so that we can infer the proper patternsMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-26Fix canonical structure resolution which was launched on the results ofMatthieu Sozeau
2014-09-25Fix incorrect assert false in detyping.Matthieu Sozeau
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-24Return a Prop not an arbitrary Type, and correct a typo.Matthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-09-23Fix bug #3656.Matthieu Sozeau
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
2014-09-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 18:35:09 +0000