aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
2016-04-27Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Hugo Herbelin
2016-04-27Revert "More abstraction in cases.mli."Hugo Herbelin
2016-04-27Revert "Add support for generalization also on named variables in pattern-mat...Hugo Herbelin
2016-04-27Revert "Add support for deep dependencies in variables within the recursive s...Hugo Herbelin
2016-04-27Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Hugo Herbelin
2016-04-27Revert "Using existing names as a basis for the inner names of the pattern-ma...Hugo Herbelin
2016-04-27Revert "Vers un filtrage profond ..."Hugo Herbelin
2016-04-27Vers un filtrage profond ...Hugo Herbelin
2016-04-27Using existing names as a basis for the inner names of the pattern-matching p...Hugo Herbelin
2016-04-27Fixing a De Bruijn bug in computing return predicate by inversion.Hugo Herbelin
2016-04-27Add support for deep dependencies in variables within the recursive structure.Hugo Herbelin
2016-04-27Add support for generalization also on named variables in pattern-matchingHugo Herbelin
2016-04-27More abstraction in cases.mli.Hugo Herbelin
2016-04-27When interpreting "match goal with ... end" in ltac, expand evars byHugo Herbelin
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
2016-04-27Optimization in building a return clause by pattern-matching: do notHugo Herbelin
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-04-05Revert "Prevent pretyping from checking well-guardedness unnecessarily."Arnaud Spiwack
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-25Fix a bug in Program coercion codeMatthieu Sozeau
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Splitting Evarutil in two distinct files.Pierre-Marie Pédrot
2016-03-20Pushing Proofview further down the dependency alley.Pierre-Marie Pédrot
2016-03-20Moving Proofview to pretyping/.Pierre-Marie Pédrot
2016-03-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-17Fix #4623: set tactic too weak with universes (regression)Maxime Dénès
2016-03-16Fix incorrect behavior of CS resolutionMatthieu Sozeau
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-28Slightly contracting code of evarconv.ml.Hugo Herbelin
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-19Adding location to universes generated by the pretyper.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 10:23:23 +0000