index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Compat
/
Coq85.v
Commit message (
Expand
)
Author
Age
*
Merge commit 'e6edb33' into v8.6
Maxime Dénès
2016-11-07
|
\
|
*
More explicit name for status of unification constraints.
Maxime Dénès
2016-11-07
*
|
Silence option deprecation warnings in the compat file
Jason Gross
2016-11-04
|
*
Add Unset Use Unif Heuristics in Compat/Coq85
Matthieu Sozeau
2016-10-22
|
/
*
Fix previous commit.
Pierre-Marie Pédrot
2016-10-17
*
Clean up type classes flags and update compat file.
Maxime Dénès
2016-10-05
*
Unbreak Ltac [ | .. | ] notation in -compat 8.5
Jason Gross
2016-09-26
*
Fix bug #4785 (use [ ] for vector nil)
Jason Gross
2016-09-26
*
no-refold patch
Paul Steckler
2016-09-09
*
Fix #4793: Coq 8.6 should accept -compat 8.6
Maxime Dénès
2016-07-06
*
Add Unset Shrink Abstract/Obligations in Coq85
Matthieu Sozeau
2016-06-27
*
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
Mode "Bracketing Last Introduction Pattern" is on for 8.4
Hugo Herbelin
2016-06-06
*
Mode "Regular Subst Tactic" is on in 8.6.
Hugo Herbelin
2016-06-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Updating Compat85.v after bd1c97653 on bracketing last or-and
Hugo Herbelin
2015-11-10
|
/
*
Add compatibility files (feature 4319)
Jason Gross
2015-09-30