coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
\| \| \| \|	The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
*	Glob-ops: a name-mapping operation for pattern-matching binders.	Arnaud Spiwack	2014-11-19
\|
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
\| \| \| \| \|	NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
*	Adding an equality function over glob_constr	Pierre-Marie Pédrot	2014-03-02
\|
*	Merging Context and Sign.	ppedrot	2013-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of name	ppedrot	2012-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a constr_pattern_eq	ppedrot	2012-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15995 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
\| \| \| \| \| \| \| \| \| \|	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
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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