coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-08-18	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin
	can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
	"pat/term" for "apply term on current_hyp as pat".
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
	- emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	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.
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	remove many excessive open Util & Errors in mli's	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 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-23	Rename rawterm.ml into glob_term.ml	glondu
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08	Using vernac parsing for Function	jforest
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13094 85f007b7-540e-0410-9357-904b9bb8a0f7