From a01a60b366307da3eca63c9937984db6f273dc41 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 25 Nov 2013 22:30:02 +0100 Subject: Getting rid of casted_open_constr. It was only used by the 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. --- lib/genarg.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/genarg.mli') diff --git a/lib/genarg.mli b/lib/genarg.mli index e2654fcf5..3d5828bbb 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -199,7 +199,7 @@ type argument_type = | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType -- cgit v1.2.3