coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A uniformization step around understand_* and interp_* functions.	herbelin	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
*	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