index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Compat
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Put plugin exports in the right compatibility file
Jason Gross
2017-06-22
*
Merge PR#375: Deprecation
Maxime Dénès
2017-06-15
|
\
*
|
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-14
|
*
Remove support for Coq 8.4.
Guillaume Melquiond
2017-06-14
|
/
*
drop vo.itarget files and compute the corresponding the corresponding values ...
Matej Kosik
2017-06-01
*
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
*
Merge PR #300 into v8.6
Pierre-Marie Pédrot
2016-10-17
|
\
*
|
Clean up type classes flags and update compat file.
Maxime Dénès
2016-10-05
|
*
Move vector/list compat notations to their relevant files
Jason Gross
2016-09-29
|
/
*
Remove spaces from around list notations
Jason Gross
2016-09-26
*
Unbreak Ltac [ | .. | ] notation in -compat 8.5
Jason Gross
2016-09-26
*
Fix bug #4785 (use [ ] for vector nil)
Jason Gross
2016-09-26
*
Refolding: disable in 8.4 compat file, document
Matthieu Sozeau
2016-09-12
*
no-refold patch
Paul Steckler
2016-09-09
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-02
|
\
|
*
Fix bug #5043: [Admitted] lemmas pick up section variables.
Pierre-Marie Pédrot
2016-08-31
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
*
|
Fix #4793: Coq 8.6 should accept -compat 8.6
Maxime Dénès
2016-07-06
|
*
Compat84: Don't mess with stdlib modules
Jason Gross
2016-07-05
*
|
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
|
*
Unbreak singleton list-like notation (-compat 8.4)
Jason Gross
2016-06-09
*
|
Relying instead on the Coq85 inclusion!
Hugo Herbelin
2016-06-06
*
|
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 remote-tracking branch 'github/pr/118' into trunk
Maxime Dénès
2016-06-06
|
\
\
*
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-20
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Removing unexcepted activation of option "Regular Subst Tactic", since
Hugo Herbelin
2016-05-14
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
|
*
|
Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...
Pierre Letouzey
2016-05-04
|
|
\
\
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-09
|
\
|
|
|
|
*
|
|
Added compatibility coercions from Specif.v which were present in Coq 8.4.
Hugo Herbelin
2016-04-08
|
*
|
|
Add -compat 8.4 econstructor tactics, and tests
Jason Gross
2016-04-05
|
*
|
|
Fix bug #4656
Jason Gross
2016-04-05
|
*
|
|
Update Coq84.v
Jason Gross
2016-04-04
|
*
|
|
Add compatibility Nonrecursive Elimination Schemes
Jason Gross
2016-04-04
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
|
*
|
|
Update copyright headers.
Maxime Dénès
2016-01-20
|
|
|
*
Update Coq84.v
Jason Gross
2016-01-12
|
|
_
|
/
|
/
|
|
|
|
*
Move compatibility notations to their proper files
Jason Gross
2015-12-29
|
|
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-15
|
\
|
|
*
Moved proof_admitted to its own file, named "AdmitAxiom.v".
Maxime Dénès
2015-12-14
*
|
Updating Compat85.v after bd1c97653 on bracketing last or-and
Hugo Herbelin
2015-11-10
|
/
*
Update compatibility file for some of bug #4392
Jason Gross
2015-11-03
*
Add compatibility files (feature 4319)
Jason Gross
2015-09-30