coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin	2014-08-18
\| \| \| \| \| \| \|	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.
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
\| \| \| \|	"pat/term" for "apply term on current_hyp as pat".
*	Fix [uconstr] name for argextend.	Arnaud Spiwack	2014-08-05
\|
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
\| \| \| \| \| \|	It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
*	Closing bug #3260	Julien Forest	2014-04-14
\| \| \| \|	adding a new grammar entry for clauses
*	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.
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
\|
*	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
\|
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
*	Removing SortArgType.	ppedrot	2013-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
\| \| \| \| \| \| \| \| \| \| \| \|	through a unique generic argument, and the level is only considered at parsing time. This may introduce unnecessary parentheses in Ltac printing though, as every tactic argument is collapsed at the lowest level. I assume this does not matter that much, and anyway Ltac printing is quite bugged as of today. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
	related types. This will ultimately allow putting genargs into these ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7