index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Partial fix for accepting bound variables with same name as implicit
herbelin
2011-05-26
*
Check if recursive calls are guarded before printing "Proof completed".
herbelin
2011-05-26
*
Fixing discriminate for identity.
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
*
Applying Enrico Tassi's patch for giving priority to delta over eta in
herbelin
2011-05-24
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...
fbesson
2011-05-23
*
ported r14149 from v8.3 branch: bug in checker (redefined global)
barras
2011-05-23
*
Restore display of notation when printing an inductive such as sig
letouzey
2011-05-21
*
added support to handle division by a constant over R
fbesson
2011-05-20
*
Remove useless "open Gc"
glondu
2011-05-19
*
Remove System.process_time (dead code)
glondu
2011-05-19
*
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
*
Coqide: allow the use of Abort (grant wish #2357)
letouzey
2011-05-18
*
Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)
letouzey
2011-05-17
*
Modops: the strengthening functions can work without any env argument
letouzey
2011-05-17
*
More work on error handling
letouzey
2011-05-17
*
Add simple test of bullet behaviour.
aspiwack
2011-05-17
*
Break circular dependency Proof_global -> Vernacexpr -> Proof_global.
aspiwack
2011-05-17
*
Fixes bug in [maximal_unfocus] introduced in r14120.
aspiwack
2011-05-17
*
Repair the "Fail" command after recent changes in exception handling
letouzey
2011-05-16
*
test-suite: no more ..._beq in the output of the search tests
letouzey
2011-05-16
*
Fix order in Search tests.
letouzey
2011-05-16
*
Fixed my last patch: these files no longer use nat_beq (automatically
vsiles
2011-05-16
*
turn the automatic generation of boolean equality
vsiles
2011-05-16
*
Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).
herbelin
2011-05-15
*
Failing instead of switching to the coercion mechanism when VMcast
herbelin
2011-05-15
*
Turning Sys_error into error by default instead of anomaly. After all,
herbelin
2011-05-15
*
A better procedure for checking presence of undefined evars.
aspiwack
2011-05-13
*
The modules in proofs now use the Errors module to explain their exceptions t...
aspiwack
2011-05-13
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
New option [Set Bullet Behavior] allows to select the behaviour of bullets.
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
*
remove useless dependancy for csdpcert
fbesson
2011-05-09
*
Fixes in the test-suite after modularisation of ZArith and co
letouzey
2011-05-06
*
Additionnal fix of romega after modularisation of ZArith
letouzey
2011-05-06
*
update of the file list in doc/stdlib
letouzey
2011-05-06
*
BinNat: N.binary_rect is now a definition instead of an opaque proof
letouzey
2011-05-05
*
Peano recursion for positive: integration of Daniel Schepler's code
letouzey
2011-05-05
*
Minimal lemmas about Z.gt, N.gt and co
letouzey
2011-05-05
*
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
*
Modularization of Nnat
letouzey
2011-05-05
*
Setoid_ring: some cleanups related with BinPos and BinNat
letouzey
2011-05-05
[prev]
[next]