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
*
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
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)
letouzey
2011-01-07
*
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
glondu
2010-12-25
*
Rename mkR* smart constructors (mostly in funind)
glondu
2010-12-25
*
s/raw/glob/g in decl_interp.ml for more consistency
glondu
2010-12-24
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename files in funind to respect new conventions
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Prepare change of nomenclature rawconstr -> glob_constr
glondu
2010-12-23
*
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
letouzey
2010-12-21
*
Remove an unused function with a Evd.fold in subtac
letouzey
2010-12-13
*
Dp: minor fix suggested by Virgile Prevosto
letouzey
2010-11-25
*
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-18
[next]