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.
---
 grammar/argextend.ml4 | 2 +-
 grammar/q_coqast.ml4  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index d884a10cbb..dc521e20d9 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -39,7 +39,7 @@ let rec make_wit loc = function
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
   | RedExprArgType -> <:expr< Constrarg.wit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
+  | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Constrarg.wit_bindings >>
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 02c00e3f0e..b405539ec9 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -207,7 +207,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
-  | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
+  | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
-- 
cgit v1.2.3