Removing RefArgType generic argument.

9 files changed, 8 insertions, 22 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index dc521e20d..934b9b117 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,7 +33,6 @@ let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
   | IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
-  | RefArgType -> <:expr< Constrarg.wit_ref >>
   | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
   | GenArgType -> <:expr< Constrarg.wit_genarg >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index b405539ec..3e11bf5a8 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -203,7 +203,6 @@ let mlexpr_of_red_expr = function
 
 let rec mlexpr_of_argtype loc = function
   | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
-  | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
   | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 97004a93d..4f20dd560 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -47,7 +47,7 @@ let wit_pattern_ident = wit_ident_gen false
 
 let wit_var = unsafe_of_type VarArgType
 
-let wit_ref = unsafe_of_type RefArgType
+let wit_ref = Genarg.make0 None "ref"
 
 let wit_quant_hyp = unsafe_of_type QuantHypArgType
 
@@ -71,6 +71,7 @@ let wit_red_expr = unsafe_of_type RedExprArgType
 (** Register location *)
 
 let () =
+  register_name0 wit_ref "Constrarg.wit_ref";
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 0f1e50568..6520669fa 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -14,7 +14,6 @@ type argument_type =
   | IntOrVarArgType
   | IdentArgType of bool
   | VarArgType
-  | RefArgType
   (* Specific types *)
   | GenArgType
   | ConstrArgType
@@ -33,7 +32,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | IntOrVarArgType, IntOrVarArgType -> true
 | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
 | VarArgType, VarArgType -> true
-| RefArgType, RefArgType -> true
 | GenArgType, GenArgType -> true
 | ConstrArgType, ConstrArgType -> true
 | ConstrMayEvalArgType, ConstrMayEvalArgType -> true
@@ -54,7 +52,6 @@ let rec pr_argument_type = function
 | IdentArgType true -> str "ident"
 | IdentArgType false -> str "pattern_ident"
 | VarArgType -> str "var"
-| RefArgType -> str "ref"
 | GenArgType -> str "genarg"
 | ConstrArgType -> str "constr"
 | ConstrMayEvalArgType -> str "constr_may_eval"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 3d5828bbb..51c261742 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -193,7 +193,6 @@ type argument_type =
   | IntOrVarArgType
   | IdentArgType of bool
   | VarArgType
-  | RefArgType
   (** Specific types *)
   | GenArgType
   | ConstrArgType
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f091a2e1d..77f5db3b4 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -148,7 +148,6 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
-  | RefArgType -> prref (out_gen (rawwit wit_ref) x)
   | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
   | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
   | ConstrMayEvalArgType ->
@@ -183,7 +182,6 @@ let rec pr_glb_generic prc prlc prtac prpat x =
   | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
-  | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x)
   | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
   | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
   | ConstrMayEvalArgType ->
@@ -219,7 +217,6 @@ let rec pr_top_generic prc prlc prtac prpat x =
   | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
   | VarArgType -> pr_id (out_gen (topwit wit_var) x)
-  | RefArgType -> pr_global (out_gen (topwit wit_ref) x)
   | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
   | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
   | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
@@ -1032,6 +1029,8 @@ let register_uniform_printer wit pr =
   Genprint.register_print0 wit pr pr pr
 
 let () =
+  Genprint.register_print0 Constrarg.wit_ref
+    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
   Genprint.register_print0 Constrarg.wit_intro_pattern
     pr_intro_pattern pr_intro_pattern pr_intro_pattern;
   Genprint.register_print0 Constrarg.wit_sort
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 19ab65d22..59bad5808 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 ce216b15d..e5f69378f 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 57aa88368..206dec104 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)