coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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".
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
\| \| \| \| \|	This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
*	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.
*	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot	2014-05-22
\|
*	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.
*	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
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
\|
*	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 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
*	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