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.
---
 interp/constrarg.ml  | 6 +-----
 interp/constrarg.mli | 4 ----
 2 files changed, 1 insertion(+), 9 deletions(-)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 16af7c3080..97004a93dd 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -60,11 +60,7 @@ let wit_constr = unsafe_of_type ConstrArgType
 
 let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
 
-let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b)
-
-let wit_open_constr = wit_open_constr_gen false
-
-let wit_casted_open_constr = wit_open_constr_gen true
+let wit_open_constr = unsafe_of_type OpenConstrArgType
 
 let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
 
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 1233e165fd..b83c20065d 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -57,12 +57,8 @@ val wit_constr_may_eval :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
   constr) genarg_type
 
-val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
 val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
 
-val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
   glob_constr_and_expr with_bindings,
-- 
cgit v1.2.3