aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\
| * evar_conv: Refine occur_rigidlyGravatar Matthieu Sozeau2016-06-13
| * Minor simplification in evarconv.Gravatar Hugo Herbelin2016-06-12
| * Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
| * Protecting eta-expansion in evarconv.ml against ill-typed problems.Gravatar Hugo Herbelin2016-06-12
* | A mini-optimization for free in unification.ml: test in O(1)Gravatar Hugo Herbelin2016-06-10
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\|
| * Fixing #4644 (regression of unification on evar-evar problems with a match).Gravatar Hugo Herbelin2016-06-09
| * Minor simplification in evarconv.ml.Gravatar Hugo Herbelin2016-06-09
| * Reverting dbdff037 which does not seem to prevent to have #3638 fixedGravatar Hugo Herbelin2016-06-09
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\|
* | More informative error message when interpreting ltac variables in terms.Gravatar Pierre-Marie Pédrot2016-05-13
| * Small optimization in evar resolution.Gravatar Pierre-Marie Pédrot2016-05-12
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Use the canonical name when looking for an eliminator (bug #4670).Gravatar Guillaume Melquiond2016-05-03
| * Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\|
| * Fix incorrect cbv reduction of primitive projections. (Bug #4634)Gravatar Guillaume Melquiond2016-04-29
* | Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Gravatar Hugo Herbelin2016-04-27
* | Revert "More abstraction in cases.mli."Gravatar Hugo Herbelin2016-04-27
* | Revert "Add support for generalization also on named variables in pattern-mat...Gravatar Hugo Herbelin2016-04-27
* | Revert "Add support for deep dependencies in variables within the recursive s...Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Gravatar Hugo Herbelin2016-04-27
* | Revert "Using existing names as a basis for the inner names of the pattern-ma...Gravatar Hugo Herbelin2016-04-27
* | Revert "Vers un filtrage profond ..."Gravatar Hugo Herbelin2016-04-27
* | Vers un filtrage profond ...Gravatar Hugo Herbelin2016-04-27
* | Using existing names as a basis for the inner names of the pattern-matching p...Gravatar Hugo Herbelin2016-04-27
* | Fixing a De Bruijn bug in computing return predicate by inversion.Gravatar Hugo Herbelin2016-04-27
* | Add support for deep dependencies in variables within the recursive structure.Gravatar Hugo Herbelin2016-04-27
* | Add support for generalization also on named variables in pattern-matchingGravatar Hugo Herbelin2016-04-27
* | More abstraction in cases.mli.Gravatar Hugo Herbelin2016-04-27
* | When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
* | Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
| * Optimization in building a return clause by pattern-matching: do notGravatar Hugo Herbelin2016-04-27
* | Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ | | |/ | |/|
* | | Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
| * | Fix a bug in Program coercion codeGravatar Matthieu Sozeau2016-03-25
* | | Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
* | | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Pushing Proofview further down the dependency alley.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Moving Proofview to pretyping/.Gravatar Pierre-Marie Pédrot2016-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 03:31:08 +0000