index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Sequent: generic equality on kernel_name replaced by kn_ord
puech
2011-07-29
*
Sequent: generic equality on constr replaced by destructors
puech
2011-07-29
*
Sequent: generic equality on ident replaced by id_ord
puech
2011-07-29
*
Instances: generic equality on global_reference replaced by RefOrdered.compare
puech
2011-07-29
*
Unify: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Integral domains
pottier
2011-07-26
*
Ring2 devient Ncring et la reification par les type classes est partagee
pottier
2011-07-26
*
Add a syntax entry for fully applied constructor pattern
pboutill
2011-07-22
*
Set Extraction KeepSingleton: an option for not decapsulating singleton types
letouzey
2011-07-04
*
Extraction: in haskell, __ may have any type, no need to unsafeCoerce it
letouzey
2011-07-04
*
Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)
letouzey
2011-07-04
*
Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml
letouzey
2011-07-04
*
Fix compilation error
msozeau
2011-06-30
*
Keep obligation source information in Program
msozeau
2011-06-30
*
update of Micromega doc
fbesson
2011-06-29
*
Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def
letouzey
2011-06-28
*
improved tactic names
fbesson
2011-06-28
*
Numbers: a particular case of div_unique
letouzey
2011-06-24
*
Follow-up concerning eqb / ltb / leb comparisons
letouzey
2011-06-21
*
Cleaning debugging printer relative to new proof engine. In
herbelin
2011-06-21
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
Fix bug 2269, program typechecker not used in Instance conclusions
msozeau
2011-06-17
*
Tests de nsatz avec la geometrie
pottier
2011-06-16
*
Moved allow_K to a unification flag
herbelin
2011-06-10
*
Call process_vernac_interp_error before calling Errors.print in
herbelin
2011-06-10
*
Revert "Check if recursive calls are guarded before printing "Proof completed"."
pboutill
2011-06-10
*
ring2, cring, nsatz avec type classe avec parametres plus notations
pottier
2011-06-10
*
Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...
msozeau
2011-06-07
*
Fix bug #2415: warn when closing modules or sections and some obligations are...
msozeau
2011-06-07
*
Check if recursive calls are guarded before printing "Proof completed".
herbelin
2011-05-26
*
Q2R -> IQR
fbesson
2011-05-25
*
Made the emacs-U option deprecated. Also removed the old code
courtieu
2011-05-24
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...
fbesson
2011-05-23
*
added support to handle division by a constant over R
fbesson
2011-05-20
*
Extraction: avoid lots of late mind_of_kn
letouzey
2011-05-19
*
Extraction: global reference should be indexed on their user part (fix #2540)
letouzey
2011-05-19
*
cbv delta - [...] before calling lia
fbesson
2011-05-18
*
apply zeta reduction before syntaxification
fbesson
2011-05-18
*
Extraction: avoid printing of Recursive Extraction in coqide's console
letouzey
2011-05-18
*
Fixed my last patch: these files no longer use nat_beq (automatically
vsiles
2011-05-16
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
Print Module (Type) M now tries to print more details
letouzey
2011-05-11
*
Improved lia + experimental nlia
fbesson
2011-05-09
*
Additionnal fix of romega after modularisation of ZArith
letouzey
2011-05-06
*
Modularisation of Znat, a few name changed elsewhere
letouzey
2011-05-05
*
BinInt: Z.add become the alternative Z.add'
letouzey
2011-05-05
*
Modularization of BinInt, related fixes in the stdlib
letouzey
2011-05-05
*
Setoid_ring: some cleanups related with BinPos and BinNat
letouzey
2011-05-05
*
Modularization of BinNat + fixes of stdlib
letouzey
2011-05-05
*
Modularization of Pnat
letouzey
2011-05-05
[next]