Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into trunk

7 files changed, 65 insertions, 30 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index ccc231cf2d..c156e869da 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -116,9 +116,23 @@ ARGUMENT EXTEND glob
 
      GLOB_TYPED AS glob_constr_and_expr
      GLOB_PRINTED BY pr_gen
-  [ lconstr(c) ] -> [ c ]
+  [ constr(c) ] -> [ c ]
 END
 
+ARGUMENT EXTEND lglob
+    PRINTED BY pr_globc
+
+     INTERPRETED BY interp_glob
+     GLOBALIZED BY glob_glob
+     SUBSTITUTED BY subst_glob
+
+     RAW_TYPED AS constr_expr
+     RAW_PRINTED BY pr_gen
+
+     GLOB_TYPED AS glob_constr_and_expr
+     GLOB_PRINTED BY pr_gen
+  [ lconstr(c) ] -> [ c ]
+END
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 1367f70324..dfc14bddf3 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -28,7 +28,14 @@ val wit_glob :
   (constr_expr,
   Tacexpr.glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+
+val wit_lglob :
+  (constr_expr,
+  Tacexpr.glob_constr_and_expr,
+  Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+
 val glob : constr_expr Pcoq.Gram.entry
+val lglob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c81e7ce3f1..031cbc7c5d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -324,8 +324,31 @@ 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) =
+  Proofview.Goal.enter (fun gl ->
+    let env = Proofview.Goal.env gl in
+    let constrvars = Tacinterp.extract_ltac_constr_values ist env in
+    let vars = (constrvars, ist.Geninterp.lfun) in
+    let c = Goal.Refinable.make begin fun h ->
+      Goal.Refinable.constr_of_raw h true true vars 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
 
 (**********************************************************************)
@@ -408,7 +431,7 @@ END
 open Tacticals
 
 TACTIC EXTEND instantiate
-  [ "instantiate" "(" integer(i) ":=" glob(c) ")" hloc(hl) ] ->
+  [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] ->
     [ Proofview.V82.tactic (instantiate i c hl)  ]
 | [ "instantiate" ] -> [ Proofview.V82.tactic (tclNORMEVAR) ]
 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..59bad5808a 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -722,8 +722,6 @@ and intern_genarg ist x =
 	(intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
   | VarArgType ->
       in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
-  | RefArgType ->
-      in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x))
   | GenArgType ->
       in_gen (glbwit wit_genarg) (intern_genarg ist (out_gen (rawwit wit_genarg) x))
   | ConstrArgType ->
@@ -736,9 +734,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))
@@ -800,6 +798,7 @@ let () =
   Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
 
 let () =
+  Genintern.register_intern0 wit_ref (lift intern_global_reference);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s))
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0821423b5d..e5f69378f4 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
@@ -1322,8 +1322,6 @@ and interp_genarg ist env sigma concl gl x =
         (interp_fresh_ident ist env (out_gen (glbwit (wit_ident_gen b)) x))
     | VarArgType ->
       in_gen (topwit wit_var) (interp_hyp ist env (out_gen (glbwit wit_var) x))
-    | RefArgType ->
-      in_gen (topwit wit_ref) (interp_reference ist env (out_gen (glbwit wit_ref) x))
     | GenArgType ->
       in_gen (topwit wit_genarg) (interp_genarg (out_gen (glbwit wit_genarg) x))
     | ConstrArgType ->
@@ -1346,13 +1344,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
@@ -1973,17 +1970,12 @@ and interp_atomic ist tac =
               end
           | VarArgType ->
               Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
-          | RefArgType ->
-              Proofview.Goal.return (
-                Value.of_constr (
-                  constr_of_global
-                    (interp_reference ist env (out_gen (glbwit wit_ref) x))))
           | GenArgType -> f (out_gen (glbwit wit_genarg) x)
           | ConstrArgType ->
               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 +2035,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."))
@@ -2154,6 +2146,8 @@ let () =
   declare_uniform wit_pre_ident str
 
 let () =
+  let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) ref) in
+  Geninterp.register_interp0 wit_ref interp;
   let interp ist gl pat = (project gl, interp_intro_pattern ist (pf_env gl) pat) in
   Geninterp.register_interp0 wit_intro_pattern interp;
   let interp ist gl s = (project gl, interp_sort s) in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 7491c9a8f8..206dec104a 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -298,9 +298,6 @@ and subst_genarg subst (x:glob_generic_argument) =
   | IdentArgType b ->
       in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x)
   | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
-  | RefArgType ->
-      in_gen (glbwit wit_ref) (subst_global_reference subst
-	(out_gen (glbwit wit_ref) x))
   | GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
   | ConstrArgType ->
       in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
@@ -312,9 +309,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))
@@ -330,6 +327,7 @@ and subst_genarg subst (x:glob_generic_argument) =
 (** Registering *)
 
 let () =
+  Genintern.register_subst0 wit_ref subst_global_reference;
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
   Genintern.register_subst0 wit_sort (fun _ v -> v)