Removing constr generic argument.

3 files changed, 5 insertions, 15 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ac0c4b266b..6f6c4a05a1 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -720,8 +720,6 @@ and intern_match_rule onlytac ist = function
 
 and intern_genarg ist x =
   match genarg_tag x with
-  | ConstrArgType ->
-    map_raw wit_constr intern_constr ist x
   | ListArgType _ ->
       let list_unpacker wit l =
         let map x =
@@ -830,6 +828,7 @@ let () =
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
+  Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
   Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c));
   Genintern.register_intern0 wit_open_constr (fun ist c -> (ist,intern_constr ist c));
   Genintern.register_intern0 wit_red_expr (lift intern_red_expr);
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index adca226303..71a6e043b5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1522,18 +1522,9 @@ and interp_genarg ist x : Val.t Ftactic.t =
     let tag = genarg_tag x in
     if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
       interp_genarg_var_list ist x
-    else match tag with
-    | ConstrArgType ->
-      Ftactic.nf_s_enter { s_enter = begin fun gl ->
-        let c = Genarg.out_gen (glbwit wit_constr) x in
-        let env = Proofview.Goal.env gl in
-        let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-        let (sigma, c) = interp_constr ist env sigma c in
-        let c = in_gen (topwit wit_constr) c in
-        Sigma.Unsafe.of_pair (Ftactic.return c, sigma)
-      end }
-    | ListArgType ConstrArgType ->
+    else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
       interp_genarg_constr_list ist x
+    else match tag with
     | ListArgType _ ->
       let list_unpacker wit l =
         let map x =
@@ -2184,6 +2175,7 @@ let () =
   Geninterp.register_interp0 wit_var (lift interp_hyp);
   Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
   Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
+  Geninterp.register_interp0 wit_constr (lifts interp_constr);
   Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
   Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
   Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0061237bf3..4f79115240 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -276,8 +276,6 @@ and subst_match_rule subst = function
 
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
-  | ConstrArgType ->
-      in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
   | ListArgType _ ->
     let list_unpacker wit l =
       let map x =
@@ -315,6 +313,7 @@ let () =
   Genintern.register_subst0 wit_var (fun _ v -> v);
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
+  Genintern.register_subst0 wit_constr subst_glob_constr;
   Genintern.register_subst0 wit_sort (fun _ v -> v);
   Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
   Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);