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
*
Little fix for Nsatz: hypotheses not directly relevant to the nsatz
herbelin
2013-05-05
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Indfun : use States.with_state_protection instead of freeze/unfreeze
letouzey
2013-04-23
*
code simplifications concerning Summary
letouzey
2013-04-22
*
More functional implementation of locality_flag and program_mode
gareuselesinge
2013-04-15
*
Backport r16394 from 8.4:
msozeau
2013-04-11
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Extraction AccessOpaque is now activated again by default (#2952)
letouzey
2013-03-18
*
Extract_env : correct exceptions mentionned in a try ... with
letouzey
2013-03-15
*
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-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
*
Recdef: an anomaly isn't so anomalous, occurs in 1618.v
letouzey
2013-03-12
*
Term.dest* functions now raise specific DestKO exn instead of Invalid_argument
letouzey
2013-03-12
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Allowing different types of, not to be mixed, generic Stores through
ppedrot
2013-03-12
*
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-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
*
Names: Modularize constant and mutual_inductive
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
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
*
Extraction: same as commit 16203, hopefully without NotASort exns
letouzey
2013-02-18
*
Fix extraction of inductive types that Coq auto-detects to be in Prop
letouzey
2013-02-14
*
No reason a priori for using unfiltered env for printing
herbelin
2013-01-29
*
Fixed synchronicity of filter with evar context in new_goal_with.
herbelin
2013-01-29
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Extraction: qualified names in Extract Constant examples (fix #2878)
letouzey
2012-12-18
*
No more constant named "int" in Coq theories (cf bug #2878)
letouzey
2012-12-18
*
Extraction of projections: restrict a hack to ocaml only (fix #2941)
letouzey
2012-12-17
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Stringset and Stringmap to String namespace.
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Ensure that a function declared with a label is used with it
letouzey
2012-12-08
*
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-17
[next]