coq - The formal proof system

Age	Commit message (Collapse)	Author
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
	native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14	Modulification of identifier	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot
	Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
	compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
	were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in ↵	letouzey
	grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
	Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02	Noise for nothing	pboutill
	Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-25	Rename mkR* smart constructors (mostly in funind)	glondu
	perl -pi -e 's/(mk)R(Ref\|Var\|Evar\|PatVar\|App\|Lambda\|Prod\|LetIn\|Case s\|LetTuple\|If\|Rec\|Sort\|Hole\|Cast\|Dynamic\|Prop\|Type\|Fix\|CoFix\|Struct Rec\|WfRec\|MeasureRec)/\1G\2/g' */.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13758 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24	More {raw => glob} changes for consistency	glondu
	perl -pi -e 's/(\W\|_)raw((?:sort\|_prop\|terms?\|_branch\|_red_flag\|pat tern\|_constr_of\|_of_pat)(?:\W\|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop\|Type\|Fix\|CoFix\|StructRec\|WfRec\|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' */.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-24	Rename files in funind to respect new conventions	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7