aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-20
|\| |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\ \ \
| | * | Fix #4623: set tactic too weak with universes (regression)Gravatar Maxime Dénès2016-03-17
| | * | Fix incorrect behavior of CS resolutionGravatar Matthieu Sozeau2016-03-16
| |/ /
| * | Try eta-expansion of records only on non-recursive onesGravatar Matthieu Sozeau2016-03-15
* | | Try eta-expansion of records only on non-recursive onesGravatar Matthieu Sozeau2016-03-14
| * | Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-09
|\| |
| * | Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\| |
* | | Slightly contracting code of evarconv.ml.Gravatar Hugo Herbelin2016-02-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 15:35:44 +0000