coq - The formal proof system

Age	Commit message (Collapse)	Author
2015-10-13	Fix some typos.	Guillaume Melquiond

2012-12-18	Modulification of name	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 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-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-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
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