index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Revert "When interpreting "match goal with ... end" in ltac, expand evars by"
Hugo Herbelin
2016-04-27
*
Revert "More abstraction in cases.mli."
Hugo Herbelin
2016-04-27
*
Revert "Add support for generalization also on named variables in pattern-mat...
Hugo Herbelin
2016-04-27
*
Revert "Add support for deep dependencies in variables within the recursive s...
Hugo Herbelin
2016-04-27
*
Revert "Fixing a De Bruijn bug in computing return predicate by inversion."
Hugo Herbelin
2016-04-27
*
Revert "Using existing names as a basis for the inner names of the pattern-ma...
Hugo Herbelin
2016-04-27
*
Revert "Vers un filtrage profond ..."
Hugo Herbelin
2016-04-27
*
Vers un filtrage profond ...
Hugo Herbelin
2016-04-27
*
Using existing names as a basis for the inner names of the pattern-matching p...
Hugo Herbelin
2016-04-27
*
Fixing a De Bruijn bug in computing return predicate by inversion.
Hugo Herbelin
2016-04-27
*
Add support for deep dependencies in variables within the recursive structure.
Hugo Herbelin
2016-04-27
*
Add support for generalization also on named variables in pattern-matching
Hugo Herbelin
2016-04-27
*
More abstraction in cases.mli.
Hugo Herbelin
2016-04-27
*
When interpreting "match goal with ... end" in ltac, expand evars by
Hugo Herbelin
2016-04-27
*
Fixing a "This clause is redundant" error when interpreting the "in"
Hugo Herbelin
2016-04-27
*
Merging the ML tactic notation and plain Tactic Notation mechanisms.
Pierre-Marie Pédrot
2016-04-25
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
*
Fixing #4677 (collision of a global variable and of a local variable
Hugo Herbelin
2016-04-19
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
\
\
|
|
|
/
|
|
/
|
*
|
|
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-25
|
*
|
Fix a bug in Program coercion code
Matthieu Sozeau
2016-03-25
*
|
|
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
2016-03-20
*
|
|
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Splitting Evarutil in two distinct files.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Pushing Proofview further down the dependency alley.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Moving Proofview to pretyping/.
Pierre-Marie Pédrot
2016-03-20
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-20
|
\
|
|
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
\
\
|
|
*
|
Fix #4623: set tactic too weak with universes (regression)
Maxime Dénès
2016-03-17
|
|
*
|
Fix incorrect behavior of CS resolution
Matthieu Sozeau
2016-03-16
|
|
/
/
|
*
|
Try eta-expansion of records only on non-recursive ones
Matthieu Sozeau
2016-03-15
*
|
|
Try eta-expansion of records only on non-recursive ones
Matthieu Sozeau
2016-03-14
|
*
|
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-09
|
\
|
|
|
*
|
Fix strategy of Keyed Unification
Matthieu Sozeau
2016-03-09
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
*
|
|
Slightly contracting code of evarconv.ml.
Hugo Herbelin
2016-02-28
|
*
|
Fix part of bug #4533: respect declared global transparency of
Matthieu Sozeau
2016-02-23
*
|
|
Adding location to universes generated by the pretyper.
Pierre-Marie Pédrot
2016-02-19
*
|
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
\
*
|
|
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
|
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
|
|
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Do not give a name to anonymous evars anymore. See bug #4547.
Pierre-Marie Pédrot
2016-02-13
|
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
|
/
/
|
/
|
|
|
*
|
Optimizing the computation of frozen evars.
Pierre-Marie Pédrot
2016-02-03
|
*
|
Opacifying the type of evar naming structure in Evd.
Pierre-Marie Pédrot
2016-02-03
|
*
|
More compact representation for evar resolvability flag.
Pierre-Marie Pédrot
2016-02-03
[next]