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.

6 files changed, 35 insertions, 17 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index ccc231cf2d..a3c531f80a 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -116,7 +116,7 @@ ARGUMENT EXTEND glob
 
      GLOB_TYPED AS glob_constr_and_expr
      GLOB_PRINTED BY pr_gen
-  [ lconstr(c) ] -> [ c ]
+  [ constr(c) ] -> [ c ]
 END
 
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c81e7ce3f1..18326435c6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -324,8 +324,27 @@ END
 
 let refine_tac = Tactics.New.refine
 
+let refine_red_flags =
+  Genredexpr.Lazy {
+    Genredexpr.rBeta=true;
+    rIota=true;
+    rZeta=false;
+    rDelta=false;
+    rConst=[];
+  }
+
+let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
+
+let refine_tac (ist, c) =
+  let c = Goal.Refinable.make begin fun h ->
+    Goal.Refinable.constr_of_raw h true true c
+  end in
+  Proofview.Goal.lift c >>= fun c ->
+  Proofview.tclSENSITIVE (Goal.refine c) <*>
+  Proofview.V82.tactic (reduce refine_red_flags refine_locs)
+
 TACTIC EXTEND refine
-  [ "refine" casted_open_constr(c) ] -> [  refine_tac c ]
+  [ "refine" glob(c) ] -> [  refine_tac c ]
 END
 
 (**********************************************************************)
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 7a0fabe1fa..2b28a65471 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -11,6 +11,6 @@ open Proof_type
 val discrHyp : Names.Id.t -> unit Proofview.tactic
 val injHyp : Names.Id.t -> unit Proofview.tactic
 
-val refine_tac : Evd.open_constr -> unit Proofview.tactic
+(* val refine_tac : Evd.open_constr -> unit Proofview.tactic *)
 
 val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 261e8583e1..19ab65d224 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -736,9 +736,9 @@ and intern_genarg ist x =
         (intern_quantified_hypothesis ist (out_gen (rawwit wit_quant_hyp) x))
   | RedExprArgType ->
       in_gen (glbwit wit_red_expr) (intern_red_expr ist (out_gen (rawwit wit_red_expr) x))
-  | OpenConstrArgType b ->
-      in_gen (glbwit (wit_open_constr_gen b))
-        ((),intern_constr ist (snd (out_gen (rawwit (wit_open_constr_gen b)) x)))
+  | OpenConstrArgType ->
+      in_gen (glbwit wit_open_constr)
+        ((),intern_constr ist (snd (out_gen (rawwit wit_open_constr) x)))
   | ConstrWithBindingsArgType ->
       in_gen (glbwit wit_constr_with_bindings)
         (intern_constr_with_bindings ist (out_gen (rawwit wit_constr_with_bindings) x))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0821423b5d..ce216b15d1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -144,7 +144,7 @@ let pr_inspect env expr result =
   let pp_result =
     if has_type result (topwit wit_tacvalue) then
     match to_tacvalue result with
-    | VRTactic _ -> str "a VRTactic"
+    | VRTactic -> str "a VRTactic"
     | VFun (_, il, ul, b) ->
       let pp_body = Pptactic.pr_glob_tactic env b in
       let pr_sep () = str ", " in
@@ -1346,13 +1346,12 @@ and interp_genarg ist env sigma concl gl x =
       in
       evdref := sigma;
       in_gen (topwit wit_red_expr) r_interp
-    | OpenConstrArgType casted ->
-      let expected_type =
-        if casted then OfType concl else WithoutTypeConstraint in
-      in_gen (topwit (wit_open_constr_gen casted))
+    | OpenConstrArgType ->
+      let expected_type = WithoutTypeConstraint in
+      in_gen (topwit wit_open_constr)
         (interp_open_constr ~expected_type
            ist env !evdref
-           (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
+           (snd (out_gen (glbwit wit_open_constr) x)))
     | ConstrWithBindingsArgType ->
       in_gen (topwit wit_constr_with_bindings)
         (pack_sigma (interp_constr_with_bindings ist env !evdref
@@ -1983,7 +1982,7 @@ and interp_atomic ist tac =
               Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) ->
               (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
-          | OpenConstrArgType false ->
+          | OpenConstrArgType ->
               Proofview.Goal.return (
                 Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) ->
               (Proofview.V82.tclEVARS sigma) <*>
@@ -2043,7 +2042,7 @@ and interp_atomic ist tac =
                 Proofview.V82.tactic (tclEVARS newsigma) <*>
                 Proofview.Goal.return v
           | QuantHypArgType | RedExprArgType
-          | OpenConstrArgType _ | ConstrWithBindingsArgType
+          | ConstrWithBindingsArgType
           | BindingsArgType
           | OptArgType _ | PairArgType _
 	    -> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations."))
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 7491c9a8f8..57aa883687 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -312,9 +312,9 @@ and subst_genarg subst (x:glob_generic_argument) =
           (out_gen (glbwit wit_quant_hyp) x))
   | RedExprArgType ->
       in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x))
-  | OpenConstrArgType b ->
-      in_gen (glbwit (wit_open_constr_gen b))
-        ((),subst_glob_constr subst (snd (out_gen (glbwit (wit_open_constr_gen b)) x)))
+  | OpenConstrArgType ->
+      in_gen (glbwit wit_open_constr)
+        ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x)))
   | ConstrWithBindingsArgType ->
       in_gen (glbwit wit_constr_with_bindings)
         (subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x))