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#605: Report a useful error for dependent induction
Maxime Dénès
2017-05-05
|
\
*
\
Merge PR#593: Functional choice <-> [inhabited] and [forall] commute
Maxime Dénès
2017-05-05
|
\
\
|
|
*
Report a useful error for dependent induction
Tej Chajed
2017-05-03
|
*
|
Functional choice <-> [inhabited] and [forall] commute
Gaetan Gilbert
2017-04-30
|
|
/
*
/
Add .dir-locals.el and _CoqProject files for emacs stdlib editing
Jason Gross
2017-04-28
|
/
*
Merge PR#584: Give andb_prop a simpler proof
Maxime Dénès
2017-04-27
|
\
*
|
Small typo in comment
Vadim Zaliva
2017-04-26
|
*
Give andb_prop a simpler proof
Jason Gross
2017-04-25
|
/
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
*
\
Merge PR#455: Farewell decl_mode
Maxime Dénès
2017-04-06
|
\
\
|
|
*
Merge branch 'origin/v8.5' into v8.6.
Hugo Herbelin
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
|
/
/
/
/
|
|
|
*
Fixing a little bug in printing ex2 (type was printed "_" by default).
Hugo Herbelin
2017-02-23
|
*
|
|
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
[next]