index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
Age
Commit message (
Expand
)
Author
2012-10-04
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-02
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-01
Ltac repeat is in fact already doing progress
letouzey
2012-09-26
Cleaning, renaming obscure functions and documenting in Hashcons.
ppedrot
2012-09-24
Fixing a bug introduced in Funind plugin when reorganizing the CList
ppedrot
2012-09-18
More cleaning in CArray...
ppedrot
2012-09-18
More cleanup of Util: utf8 aspects moved to a new file unicode.ml
letouzey
2012-09-18
Cleaning interface of Util.
ppedrot
2012-09-17
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-15
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-14
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-13
Made Pp.std_ppcmds opaque.
ppedrot
2012-08-24
Fix Extraction Implicit on axioms.
aspiwack
2012-08-24
Experimental support for a comment in the files' preamble in extraction.
aspiwack
2012-08-24
Add option Set/Unset Extraction Conservative Types.
aspiwack
2012-08-08
Updating headers.
herbelin
2012-08-08
Fixup for macOS 10.8 & Ocaml 4.0
pboutill
2012-08-06
Vecnacentries.dump_global silently ignores exceptions
pboutill
2012-08-06
Try to make the use of Unix.lockf in micromega compatible with Win32
letouzey
2012-08-05
Dump references in Extraction
pboutill
2012-08-05
Dump references
pboutill
2012-08-02
Bigint: new functions of_int and to_int, 2nd arg of pow in int
letouzey
2012-07-19
Getting rid of the undocumented [complete] tactic, which was
ppedrot
2012-07-13
Fixes r15610 (A new status Unsafe in Interface).
aspiwack
2012-07-07
Ring_polynom : a restricted simpl instead of a unfold;fold
letouzey
2012-07-05
Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)
letouzey
2012-07-05
Legacy Ring and Legacy Field migrated to contribs
letouzey
2012-07-05
rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite
letouzey
2012-07-05
More cleanup in Ring_polynom and EnvRing
letouzey
2012-07-05
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-06-28
Cleaning opening of the standard List module.
ppedrot
2012-06-28
Replace nat indices with positive one in Btauto.
ppedrot
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-14
Internalization of pattern is done in two phases.
pboutill
2012-06-12
Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.
ppedrot
2012-06-01
More cleaning
ppedrot
2012-06-01
Cleaning Pp.ppnl use
ppedrot
2012-06-01
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-05-30
Getting rid of Pp.msg
ppedrot
2012-05-30
More uniformisation in Pp.warn functions.
ppedrot
2012-05-29
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
place all files specific to camlp4 syntax extensions in grammar/
letouzey
2012-05-29
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
[next]