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
*
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
*
Modularization of BinPos + fixes in Stdlib
letouzey
2011-05-05
*
Definitions of positive, N, Z moved in Numbers/BinNums.v
letouzey
2011-05-05
*
Extraction: allow extraction foo when foo is an alias notation
letouzey
2011-05-05
*
First phase removing obsolete support for eta up to conversion in
herbelin
2011-05-04
*
Fixed a bug causing inconsistent states during proof editting.
aspiwack
2011-04-29
*
bug fix: concurrent access of persistent_cache
fbesson
2011-04-21
*
Declarative mode: fix escape and return.
aspiwack
2011-04-19
*
Extraction: nicer error when a toplevel module has no body (#2525)
letouzey
2011-04-15
*
Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)
letouzey
2011-04-15
*
Extraction: opaque terms are not traversed anymore by default
letouzey
2011-04-13
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
Extraction: unfolds the let-in created by Program when handling "match"
letouzey
2011-04-07
*
Extraction: avoid some useless Obj.magic by fixing my ML type unifier
letouzey
2011-04-07
*
Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.
aspiwack
2011-04-06
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Quickly avoid global axioms in Loic new files about ring
letouzey
2011-04-03
*
Extraction: customized inductives are always standard
glondu
2011-03-31
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Keep information on which fields are subclasses in class declarations,
msozeau
2011-03-11
*
Tentative to make unification check types at every instanciation of an
msozeau
2011-03-11
*
syntax for exponents
pottier
2011-03-08
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
Extraction: a warning when an opaque constant is enterred
letouzey
2011-03-07
*
Extraction: fix printing of haskell modular names
letouzey
2011-03-07
*
Extraction: avoid printing unused mutual fix components (fix #2477)
letouzey
2011-03-07
*
A new command "Separate Extraction"
letouzey
2011-03-07
*
Improved define_evar_as_lambda which was creating an unrelated new evar
herbelin
2011-03-05
*
Extraction: improved indentation of extracted code (fix #2497)
letouzey
2011-03-04
*
Add a flag to hide obligations in Program-generated terms under an
msozeau
2011-02-28
*
Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)
letouzey
2011-02-25
*
Fix indentation of default pattern in haskell case (bug #2476)
letouzey
2011-02-25
*
Revert "syntax for exponents"
glondu
2011-02-25
*
syntax for exponents
pottier
2011-02-22
*
anneaux commutatifs ou non, reification sans ml
pottier
2011-02-22
*
Interp a definition with the implicit arguments of its local context
pboutill
2011-02-10
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
Started to fix the declarative proof mode (C-zar).
aspiwack
2011-02-10
*
Dp: another fix suggested by Virgile Prevosto
letouzey
2011-02-03
[next]