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
...
*
Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...
Guillaume Melquiond
2014-04-22
*
Fixing missing headers.
Hugo Herbelin
2014-04-16
*
No more Coersion in Init.
Pierre Boutillier
2014-04-10
*
Define [projT3] and [proj3_sig]
Jason Gross
2014-04-10
*
Closing bug #3164
Julien Forest
2014-04-04
*
Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.
Guillaume Melquiond
2014-03-10
*
Pos.compare_cont takes the comparison as first argument
Pierre Boutillier
2014-02-28
*
fixup complement Fin
Pierre Boutillier
2014-02-24
*
Less dependencies in Omega.
Pierre-Marie Pédrot
2014-02-08
*
FinFun.v: results about injective/surjective/bijective fonctions over finite ...
Pierre Letouzey
2014-02-07
*
[Coercion]s use [Sortclass], not [Prop] (in docs)
Jason Gross
2014-01-24
*
List: Bug 3039 weaker requirement for fold symmetric
Pierre Boutillier
2013-12-20
*
Better unification for [projT1] and [proj1_sig].
Jason Gross
2013-12-12
*
Generalize eq_proofs_unicity
Jason Gross
2013-12-12
*
Improved the presentation of the proof of UIP_refl_nat.
Hugo Herbelin
2013-12-04
*
Add lemma derivable_pt_lim_atan.
Guillaume Melquiond
2013-12-04
*
Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.
Guillaume Melquiond
2013-12-03
*
Remove a useless hypothesis from Rle_Rinv.
Guillaume Melquiond
2013-12-03
*
Adding Acc_intro_generator in order to help computations of Function in parti...
forest
2013-11-20
*
Nicer infered names in refine.
aspiwack
2013-11-04
*
Restore Zsqrt compat now that refine works fine with match.
aspiwack
2013-11-02
*
A whole new implemenation of the refine tactic.
aspiwack
2013-11-02
*
Side effect free implementation of admit (Isabelle's oracle)
gareuselesinge
2013-08-08
*
Adding a dependent version of equal_f, thus fixing #3074.
ppedrot
2013-08-02
*
Typo in definition clos_refl
ppedrot
2013-07-31
*
Fixing #3089. This implied tweaking the definition of the lexicographic
ppedrot
2013-07-26
*
Added a concat function to List theory. Strangely, it was missing.
ppedrot
2013-07-24
*
"Boolean Equality" and "Case Analysis" are already off by default...
letouzey
2013-07-17
*
More dynamic argument scopes
letouzey
2013-07-17
*
A constructive proof of Fan theorem where paths are represented by predicates.
herbelin
2013-06-02
*
Making the behavior of "injection ... as ..." more natural:
herbelin
2013-06-02
*
Improving printing of 'rew' notation
herbelin
2013-05-05
*
Relaxing the constraint on eta-expanding on the fly while looking for
herbelin
2013-05-05
*
Added group properties of eq_refl, eq_sym, eq_trans
herbelin
2013-04-17
*
Normalized type for Vector.map2
pboutill
2013-03-25
*
NMake*: avoid some warning about Let outside sections
letouzey
2013-03-22
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
2013-03-21
*
cbn friendly VectorDef
pboutill
2013-02-25
*
make validate repaired via a temporary fix for #2949
letouzey
2013-02-13
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
nat_iter n f x -> nat_rect _ x (fun _ => f) n
pboutill
2012-12-21
*
Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)
letouzey
2012-12-18
*
No more constant named "int" in Coq theories (cf bug #2878)
letouzey
2012-12-18
*
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-12-08
*
Making subset_eq_compat applying over more general domain "Type" (see #2938).
herbelin
2012-12-05
*
Identities over types satisfying Uniqueness of Identity Proofs
herbelin
2012-12-04
*
Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing
herbelin
2012-11-15
*
Some lemmas on property of rewriting. It will probably be worth at
herbelin
2012-11-15
*
Added a proof that Prop<>Type, for arbitrary fixed Type.
herbelin
2012-11-15
*
A decidability property of functional relations over decidable codomains.
herbelin
2012-11-15
[prev]
[next]