coq - The formal proof system

Age	Commit message (Expand)	Author
2013-06-21	Revert "parse "of" as KEYID "of""	gareuselesinge
2013-06-19	parse "of" as KEYID "of"	gareuselesinge
2013-06-18	Removing the various glob/subst/interp registering functions for	ppedrot
2013-06-10	Hiding tactic value representations.	ppedrot
2013-06-06	Uniformizing generic argument types.	ppedrot
2013-06-05	Replacing lists by maps in matching interpretation.	ppedrot
2013-05-30	bwaa, a Pervasive.compare	pboutill
2013-05-29	newring.ml4: interp constr arg at interp time (not parse time)	gareuselesinge
2013-05-12	Removing Gmap from Extraction plugin	ppedrot
2013-05-12	Use the Hook module here and there.	ppedrot
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-08	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot
2013-05-06	States: frozen states can hold closures	gareuselesinge
2013-05-05	Little fix for Nsatz: hypotheses not directly relevant to the nsatz	herbelin
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-15	More functional implementation of locality_flag and program_mode	gareuselesinge
2013-04-11	Backport r16394 from 8.4:	msozeau
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-18	Extraction AccessOpaque is now activated again by default (#2952)	letouzey
2013-03-15	Extract_env : correct exceptions mentionned in a try ... with	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-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-12	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-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-26	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey
2013-02-26	Names: Modularize constant and mutual_inductive	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-19	Classops : avoid some use of Gmap	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-02-18	Extraction: same as commit 16203, hopefully without NotASort exns	letouzey
2013-02-14	Fix extraction of inductive types that Coq auto-detects to be in Prop	letouzey
2013-01-29	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-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes