Removing constr generic argument.

11 files changed, 19 insertions, 39 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cbebcdfcd..cc1cf23d6 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -510,7 +510,7 @@ let _ =
   try
     Vernacinterp.vinterp_add false ("PrintConstr", 0)
       (function
-         [c] when genarg_tag c = ConstrArgType && true ->
+         [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
@@ -526,7 +526,7 @@ let _ =
   try
     Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
       (function
-         [c] when genarg_tag c = ConstrArgType && true ->
+         [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 9abe5d7cf..cb006186a 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -30,7 +30,6 @@ let mk_extraarg loc s =
     <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
-  | ConstrArgType -> <:expr< Constrarg.wit_constr >>
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
   | PairArgType (t1,t2) ->
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 798d428e9..e11b37fc0 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -223,7 +223,6 @@ let mlexpr_of_red_expr = function
       <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
-  | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
   | Genarg.PairArgType (t1,t2) ->
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 94c13fe79..a8dfd02e1 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -44,7 +44,8 @@ let wit_quant_hyp = Genarg.make0 None "quant_hyp"
 let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
   Genarg.make0 None "sort"
 
-let wit_constr = unsafe_of_type ConstrArgType
+let wit_constr =
+  Genarg.make0 None "constr"
 
 let wit_constr_may_eval =
   Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
@@ -75,6 +76,7 @@ let () =
   register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
+  register_name0 wit_constr "Constrarg.wit_constr";
   register_name0 wit_uconstr "Constrarg.wit_uconstr";
   register_name0 wit_open_constr "Constrarg.wit_open_constr";
   register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval";
diff --git a/lib/genarg.ml b/lib/genarg.ml
index af9ea70ec..c2c1014f1 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -57,14 +57,12 @@ end
 
 type argument_type =
   (* Specific types *)
-  | ConstrArgType
   | ListArgType of argument_type
   | OptArgType of argument_type
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
 let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| ConstrArgType, ConstrArgType -> true
 | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
 | PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) ->
@@ -73,7 +71,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | _ -> false
 
 let rec pr_argument_type = function
-| ConstrArgType -> str "constr"
 | ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
 | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
 | PairArgType (t1, t2) ->
@@ -190,19 +187,12 @@ let default_empty_value t =
       | _ -> None)
   | ExtraArgType s ->
     (String.Map.find s !arg0_map).nil
-  | _ -> None in
+  in
   match aux t with
   | Some v -> Some (Obj.obj v)
   | None -> None
 
-(** Beware: keep in sync with the corresponding types *)
-let base_create n = Val.Base (Dyn.create n)
-let genarg_T = base_create "genarg"
-let constr_T = base_create "constr"
-
 let rec val_tag = function
-  (** Must ensure that toplevel types of Var and Ident agree! *)
-| ConstrArgType -> cast_tag constr_T
 | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn
 | ListArgType t -> cast_tag (Val.List (val_tag t))
 | OptArgType t -> cast_tag (Val.Opt (val_tag t))
@@ -222,7 +212,6 @@ let try_prj wit v = match prj (val_tag wit) v with
 
 let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a =
 fun wit v -> match unquote wit with
-| ConstrArgType
 | ExtraArgType _ -> try_prj wit v
 | ListArgType t ->
   let Val.Dyn (tag, v) = v in
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 8d929f9f6..56c09f14f 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -211,8 +211,6 @@ val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a
 (** {6 Type reification} *)
 
 type argument_type =
-  (** Basic types *)
-  | ConstrArgType
   (** Specific types *)
   | ListArgType of argument_type
   | OptArgType of argument_type
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index df0d26206..3ed530425 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -272,7 +272,7 @@ let create_entry u s etyp =
     new_entry etyp u s
 
 let create_constr_entry s =
-  outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType)
+  outGramObj (rawwit wit_constr) (create_entry uconstr s (unquote (rawwit wit_constr)))
 
 let create_generic_entry s wit =
   outGramObj wit (create_entry utactic s (unquote wit))
@@ -633,7 +633,7 @@ let compute_entry allow_create adjust forpat = function
       let u = get_univ u in
       let e =
         try get_entry u n
-        with Not_found when allow_create -> create_entry u n ConstrArgType in
+        with Not_found when allow_create -> create_entry u n (unquote (rawwit wit_constr)) in
       object_of_typed_entry e, None, true
 
 (* This computes the name of the level where to add a new rule *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index df5f57dac..a8fa8313f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -267,7 +267,6 @@ module Make
 
   let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
     match Genarg.genarg_tag x with
-      | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
       | ListArgType _ ->
         let list_unpacker wit l =
           let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
@@ -295,7 +294,6 @@ module Make
 
   let rec pr_glb_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
       | ListArgType _ ->
         let list_unpacker wit l =
           let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
@@ -322,7 +320,6 @@ module Make
 
   let rec pr_top_generic_rec prc prlc prtac prpat x =
     match Genarg.genarg_tag x with
-      | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
       | ListArgType _ ->
         let list_unpacker wit l =
           let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
@@ -1427,6 +1424,12 @@ let () =
   Genprint.register_print0 Constrarg.wit_sort
     pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
   Genprint.register_print0
+    Constrarg.wit_constr
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> Printer.pr_glob_constr c)
+    Printer.pr_constr
+  ;
+  Genprint.register_print0
     Constrarg.wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ac0c4b266..6f6c4a05a 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 adca22630..71a6e043b 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 0061237bf..4f7911524 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);