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.
---
 parsing/g_tactic.ml4 | 5 +----
 parsing/pcoq.ml4     | 4 +---
 parsing/pcoq.mli     | 1 -
 3 files changed, 2 insertions(+), 8 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index eb483c50cf..93afb3d5ae 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -215,7 +215,7 @@ let merge_occurrences loc cl = function
 
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-  bindings red_expr int_or_var open_constr casted_open_constr
+  bindings red_expr int_or_var open_constr
   simple_intropattern;
 
   int_or_var:
@@ -236,9 +236,6 @@ GEXTEND Gram
   open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
-  casted_open_constr:
-    [ [ c = constr -> ((),c) ] ]
-  ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
       | c = constr_with_bindings -> induction_arg_of_constr c
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 79228e9462..d25efa72a8 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -377,9 +377,7 @@ module Tactic =
     (* Entries that can be refered via the string -> Gram.entry table *)
     (* Typically for tactic user extensions *)
     let open_constr =
-      make_gen_entry utactic (rawwit (wit_open_constr_gen false)) "open_constr"
-    let casted_open_constr =
-      make_gen_entry utactic (rawwit (wit_open_constr_gen true)) "casted_open_constr"
+      make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
     let constr_with_bindings =
       make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
     let bindings =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index bbb71a1703..56282f2f67 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -213,7 +213,6 @@ module Tactic :
   sig
     open Glob_term
     val open_constr : open_constr_expr Gram.entry
-    val casted_open_constr : open_constr_expr Gram.entry
     val constr_with_bindings : constr_expr with_bindings Gram.entry
     val bindings : constr_expr bindings Gram.entry
     val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
-- 
cgit v1.2.3