aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2014-09-06Cleanup code for looking up projection bodies.Matthieu Sozeau
2014-09-05The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex...Arnaud Spiwack
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-09-04Add test-suite file for Case derivation on primitive records.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
2014-09-02Fixing bug #3136.Pierre-Marie Pédrot
2014-09-01In evarconv, do first-order unification of LetIn's properly, ensuring we comp...Matthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
2014-08-28There are some occurs-check cases that can be handled by imitation (using pru...Matthieu Sozeau
2014-08-28Fixing an unnatural selection of subterms larger than expected in theHugo Herbelin
2014-08-26Debug RAKAMPierre Boutillier
2014-08-26Make evarconv and unification able to handle eta for records in presenceMatthieu Sozeau
2014-08-26Fix compilation error due to commented code in previous commit by Hugo.Matthieu Sozeau
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-08-18Fixing unification of subterms identified by patterns.Hugo Herbelin
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
2014-08-14Remove confusing behavior of unify_with_subterm that could fail withMatthieu Sozeau
2014-08-14Fix non-printing of coercions for primitive projections (fixes bug #3433).Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-08-10Fix bug introduced by earlier commit on first-order unification of primitiveMatthieu Sozeau
2014-08-09Fix unification which was failing when unifying a primitive projection againstMatthieu Sozeau
2014-08-09Allow pattern matching on the applied form of projections with primitiveMatthieu Sozeau
2014-08-09Do early occur-check in unification to allow eta to fire (fixes bug #3477)Matthieu Sozeau
2014-08-09Using the asymmetric merging primitive in Evd.Pierre-Marie Pédrot
2014-08-09Cleaning up interface of ContextSet.Pierre-Marie Pédrot
2014-08-09Tentative performance fix for Evd.merge_uctx.Pierre-Marie Pédrot
2014-08-08Fix evarconv not applying eta when it used to. Fixes bug#3319.Matthieu Sozeau
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-08-05Small code simplification.Pierre-Marie Pédrot
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-08-03- Fix handling of opaque polymorphic definitions which were turned transparent.Matthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-08-03- Fix has_undefined_evars not using its or_sorts argument anymore.Matthieu Sozeau
2014-08-01Continuing (incomplete) cleaning of Inductiveops.Hugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-07-31Add an option to solve typeclass goals generated by apply which can't beMatthieu Sozeau
2014-07-30Avoid introducing additional universes when doing pruning in evarsolve.Matthieu Sozeau
2014-07-29Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 09:14:22 +0000