Removing RefArgType generic argument.

3 files changed, 4 insertions, 12 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 19ab65d224..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 ->
@@ -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 ce216b15d1..e5f69378f4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -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 ->
@@ -1972,11 +1970,6 @@ 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) ->
@@ -2153,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 57aa883687..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))
@@ -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)