index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
Added a Register Inline command for the native compiler. Will be ported to th...
mdenes
2013-07-10
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
Use definition_entry to declare local definitions
gareuselesinge
2013-05-09
*
Cosmetic change
gareuselesinge
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Summary: support selective freeze
gareuselesinge
2013-05-06
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Fix issues with "Reset Initial" in scripts given to coqtop -l
letouzey
2013-04-23
*
coqtop -compile: avoid with_heavy_rollback when non-interactive
letouzey
2013-04-23
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Declaremods: some more minor cleanup
letouzey
2013-04-22
*
Minor simplifications in Declaremods and Safe_typing
letouzey
2013-04-15
*
Declaremods: drop some useless stuff (slight gain in vo size)
letouzey
2013-04-15
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Safe_typing+Libary: use some arrays instead of lists in vo structures
letouzey
2013-03-28
*
Synchronizing loadpath with the backtrack mechanism.
ppedrot
2013-03-26
*
Moved the Loadpath part of Library to its own file, and documented
ppedrot
2013-03-26
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Removing mandatory suffixes for library files.
ppedrot
2013-03-21
*
Modules and ppvernac, sequel of Enrico's commit 16261
letouzey
2013-03-13
*
Declaremods: a few syntactic improvements
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 8)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 6)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 5)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 1)
letouzey
2013-03-12
*
Added a Local Definition vernacular command. This type of definition
ppedrot
2013-03-11
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Mod_subst: misc reformulations
letouzey
2013-02-26
*
Reduced the noise level when dynlinking in bytecode mode or when
mdenes
2013-02-24
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Dir_path --> DirPath
letouzey
2013-02-19
*
module_path --> ModPath.t, kernel_name --> KerName.t
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
letouzey
2013-02-19
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)
herbelin
2013-02-01
*
Fixed bug #2966 (de Bruijn error in computation of heads for coercions).
herbelin
2013-01-28
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Improving formatting of output of "Test table".
herbelin
2013-01-27
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
[next]