index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
Commit message (
Expand
)
Author
Age
*
Merge PR#455: Farewell decl_mode
Maxime Dénès
2017-04-06
|
\
*
\
Merge PR#442: Allow interactive editing of Coq.Init.Logic
Maxime Dénès
2017-03-17
|
\
\
*
\
\
Merge PR#451: Add η principles for sigma types
Maxime Dénès
2017-03-17
|
\
\
\
|
|
|
*
Farewell decl_mode
Enrico Tassi
2017-03-07
|
|
_
|
/
|
/
|
|
*
|
|
A couple of other useful properties about compare_cont.
Hugo Herbelin
2017-03-03
*
|
|
Compatibility of iff wrt not and imp.
Hugo Herbelin
2017-03-03
|
*
|
Add η principles for sigma types
Jason Gross
2017-03-01
|
*
|
Remove some trailing whitespace in Init/Specif.v
Jason Gross
2017-03-01
|
/
/
|
*
Allow interactive editing of Coq.Init.Logic
Jason Gross
2017-02-21
|
/
*
Ltac as a plugin.
Pierre-Marie Pédrot
2017-02-17
*
Remove v62 from stdlib.
Théo Zimmermann
2016-10-24
*
Replacing deprecated Implicit Arguments in prelude.
Maxime Dénès
2016-07-18
*
Remove the swap tactic from the prelude.
Maxime Dénès
2016-07-18
*
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
Adding option "Set Reversible Pattern Implicit" to Specif.v so that an
Hugo Herbelin
2016-06-16
*
Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"
Hugo Herbelin
2016-04-27
*
Adding option "Set Reversible Pattern Implicit" to Specif.v so that an
Hugo Herbelin
2016-04-27
*
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
*
|
Moving Eauto to a simple ML file.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving tauto.ml4 to a proper ML file.
Pierre-Marie Pédrot
2016-02-23
*
|
Moving the Tauto tactic to proper Ltac.
Pierre-Marie Pédrot
2016-02-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
\
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
Removing auto from the tactic AST.
Pierre-Marie Pédrot
2015-12-24
|
*
|
Remove Print Universe directive.
Matthieu Sozeau
2015-10-02
|
*
|
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
|
|
*
Move type_scope into user space, fix some output logs
Jason Gross
2015-08-14
|
|
*
Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080
Jason Gross
2015-08-14
|
|
/
|
/
|
|
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
|
*
Adding a notation { x & P } for { x : _ & P }.
Hugo Herbelin
2015-08-02
*
|
Tentatively setting cons and Some with 1st implicit argument maximal
Hugo Herbelin
2015-05-09
|
/
*
Fix various typos in documentation
Matěj Grabovský
2015-03-31
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Reorder the steps of the easy tactic. (Fix for bug #2630)
Guillaume Melquiond
2015-02-25
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
*
Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".
Hugo Herbelin
2014-11-02
*
eta contractions
Pierre Boutillier
2014-10-01
*
- Fix printing and parsing of primitive projections, including the Set
Matthieu Sozeau
2014-09-09
*
Removing the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Instead of relying on a trick to make the constructor tactic parse, put
Pierre-Marie Pédrot
2014-08-07
*
Removing the "constructor" tactic from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-07-09
*
Basic lemmas about the algebraic structure of equality.
Hugo Herbelin
2014-05-31
*
Moving argument-free tactics out of the AST into a dedicated
Pierre-Marie Pédrot
2014-05-16
*
Now parsing rules of ML-declared tactics are only made available after the
Pierre-Marie Pédrot
2014-05-12
*
Removing comment outdated since eta holds in conversion rule (this
Hugo Herbelin
2014-05-07
[next]