index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
funind
Age
Commit message (
Expand
)
Author
2013-05-09
Use definition_entry to declare local definitions
gareuselesinge
2013-05-09
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-06
States: frozen states can hold closures
gareuselesinge
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-23
Indfun : use States.with_state_protection instead of freeze/unfreeze
letouzey
2013-04-22
code simplifications concerning Summary
letouzey
2013-04-02
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 15)
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 11)
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 7)
letouzey
2013-03-12
Recdef: an anomaly isn't so anomalous, occurs in 1618.v
letouzey
2013-03-12
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-11
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-02-26
kernel/declarations becomes a pure mli
letouzey
2013-02-19
Dir_path --> DirPath
letouzey
2013-02-18
use List.rev_map whenever possible
letouzey
2013-02-18
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-01-28
Uniformization of the "anomaly" command.
ppedrot
2013-01-22
New implementation of the conversion test, using normalization by evaluation to
mdenes
2012-12-18
Modulification of name
ppedrot
2012-12-18
Modulification of Label
ppedrot
2012-12-14
Modulification of dir_path
ppedrot
2012-12-14
Modulification of identifier
ppedrot
2012-12-14
Moved Intset and Intmap to Int namespace.
ppedrot
2012-11-17
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-08
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-10-31
correcting a little bug in Function
jforest
2012-10-06
still some more dead code removal
letouzey
2012-10-06
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
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-09-24
Fixing a bug introduced in Funind plugin when reorganizing the CList
ppedrot
2012-09-18
More cleaning in CArray...
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-08-08
Updating headers.
herbelin
2012-08-08
Fixup for macOS 10.8 & Ocaml 4.0
pboutill
2012-07-13
Fixes r15610 (A new status Unsafe in Interface).
aspiwack
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-01
More cleaning
ppedrot
2012-06-01
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-05-30
Getting rid of Pp.msg
ppedrot
[next]