index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
Fix to previous commit (ClassicalFacts.v).
Hugo Herbelin
2015-12-05
*
|
Adding proofs on the relation between excluded-middle and minimization.
Hugo Herbelin
2015-12-05
*
|
Experimenting removing strong normalization of the mid-statement in tactic cut.
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
*
|
Updating Compat85.v after bd1c97653 on bracketing last or-and
Hugo Herbelin
2015-11-10
*
|
Adding an amazing property of Prop.
Hugo Herbelin
2015-11-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Update compatibility file for some of bug #4392
Jason Gross
2015-11-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Remove the "exists" overrides from Program. (Fix bug #4360)
Guillaume Melquiond
2015-10-07
|
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
\
|
|
*
Remove Print Universe directive.
Matthieu Sozeau
2015-10-02
|
|
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
|
|
/
|
*
Add compatibility files (feature 4319)
Jason Gross
2015-09-30
*
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Hugo Herbelin
2015-09-09
|
\
|
|
*
Emphasizing that eta for vectors is an instance of caseS, as pointed
Hugo Herbelin
2015-09-08
|
*
Minor modifications to WeakFanTheorem.
Hugo Herbelin
2015-09-08
|
*
Adding a proof of eta on Vector.t of non-zero size.
Hugo Herbelin
2015-09-08
*
|
Adding a proof of surjective pairing on vectors.
Hugo Herbelin
2015-08-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-05
|
\
|
|
*
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
|
*
Remove some outdated files and fix permissions.
Guillaume Melquiond
2015-07-31
*
|
Merge remote-tracking branch 'forge/v8.5'
Pierre Boutillier
2015-06-22
|
\
|
|
*
The "on_last_hyp" tactic now behaves as it should.
Cyprien Mangin
2015-06-12
*
|
Merge v8.5 into trunk
Hugo Herbelin
2015-05-15
|
\
|
|
*
List.nth_error directly produces Some/None instead of value/error
Pierre Letouzey
2015-05-12
|
*
Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)
Guillaume Melquiond
2015-05-12
*
|
Tentatively setting cons and Some with 1st implicit argument maximal
Hugo Herbelin
2015-05-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
|
\
|
|
*
Giving to "subst" a more natural semantic (fixing #4214) by using all
Hugo Herbelin
2015-05-01
*
|
Merge branch 'v8.5' into trunk
Pierre Letouzey
2015-04-09
|
\
|
|
*
Prove [map_ext] using [map_ext_in].
Nickolai Zeldovich
2015-04-09
|
*
Add a [map_ext_in] lemma to List.v.
Nickolai Zeldovich
2015-04-09
|
*
Fix instances of universe-polymorphic generalized rewriting to avoid
Matthieu Sozeau
2015-04-09
|
*
MMapAVL: some improved proofs + fix a forgotten Admitted
Pierre Letouzey
2015-04-02
|
*
MMapAVL: implementing MMapInterface via AVL trees
Pierre Letouzey
2015-04-02
|
*
ZArith/Int.v: some modernizations
Pierre Letouzey
2015-04-02
[next]