coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
\| \| \| \| \| \|	Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
\| \| \| \| \| \| \| \| \|	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
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
\| \| \| \| \| \| \|	No good reason for that except uniformity so revert this commit if you find a reason against it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Second step of integration of Program:	msozeau	2012-03-14
\| \| \| \| \| \| \| \|	- Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Noise for nothing	pboutill	2012-03-02
\| \| \| \| \| \| \| \| \| \| \|	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
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction du bug 2047	jforest	2011-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14465 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A new mechanism to handle errors.	aspiwack	2011-05-13
\| \| \| \| \| \| \|	Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
\| \| \| \| \| \| \| \|	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
*	More {raw => glob} changes for consistency	glondu	2010-12-24
\| \| \| \| \| \| \| \| \|	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
*	Rename files in funind to respect new conventions	glondu	2010-12-24
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7