Removing the special status of open_constr generic argument.

We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.

12 files changed, 15 insertions, 34 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 87a0dfa98..f6c223b74 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,7 +33,6 @@ let rec make_wit loc = function
   | IdentArgType -> <:expr< Constrarg.wit_ident >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
   | ConstrArgType -> <:expr< Constrarg.wit_constr >>
-  | OpenConstrArgType -> <:expr< Constrarg.wit_open_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 fc08f0a49..494ec6ba2 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -225,7 +225,6 @@ let mlexpr_of_red_expr = function
 let rec mlexpr_of_argtype loc = function
   | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
-  | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | 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$ >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ab54b6197..44623f9c9 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -49,7 +49,7 @@ let wit_constr_may_eval =
 
 let wit_uconstr = Genarg.make0 None "uconstr"
 
-let wit_open_constr = unsafe_of_type OpenConstrArgType
+let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr"
 
 let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings"
 
@@ -72,6 +72,7 @@ let () =
   register_name0 wit_tactic "Constrarg.wit_tactic";
   register_name0 wit_sort "Constrarg.wit_sort";
   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";
   register_name0 wit_red_expr "Constrarg.wit_red_expr";
   register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 052e4ec69..0cc111e61 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -50,7 +50,7 @@ val wit_constr_may_eval :
 val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
-  (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
+  (constr_expr, glob_constr_and_expr, constr) genarg_type
 
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 2b8e0c9fd..6108c1555 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -61,7 +61,6 @@ type argument_type =
   | VarArgType
   (* Specific types *)
   | ConstrArgType
-  | OpenConstrArgType
   | ListArgType of argument_type
   | OptArgType of argument_type
   | PairArgType of argument_type * argument_type
@@ -71,7 +70,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | IdentArgType, IdentArgType -> true
 | VarArgType, VarArgType -> true
 | ConstrArgType, ConstrArgType -> true
-| OpenConstrArgType, OpenConstrArgType -> 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) ->
@@ -83,7 +81,6 @@ let rec pr_argument_type = function
 | IdentArgType -> str "ident"
 | VarArgType -> str "var"
 | ConstrArgType -> str "constr"
-| OpenConstrArgType -> str "open_constr"
 | ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
 | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
 | PairArgType (t1, t2) ->
@@ -210,14 +207,12 @@ let base_create n = Val.Base (Dyn.create n)
 let ident_T = base_create "ident"
 let genarg_T = base_create "genarg"
 let constr_T = base_create "constr"
-let open_constr_T = base_create "open_constr"
 
 let rec val_tag = function
 | IdentArgType -> cast_tag ident_T
 | VarArgType -> cast_tag ident_T
   (** Must ensure that toplevel types of Var and Ident agree! *)
 | ConstrArgType -> cast_tag constr_T
-| OpenConstrArgType -> cast_tag open_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))
@@ -240,7 +235,7 @@ fun wit v -> match unquote wit with
 | IdentArgType
 | VarArgType
 | ConstrArgType
-| OpenConstrArgType | ExtraArgType _ -> try_prj wit v
+| ExtraArgType _ -> try_prj wit v
 | ListArgType t ->
   let Val.Dyn (tag, v) = v in
   begin match tag with
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 090496093..674ee97ae 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -216,7 +216,6 @@ type argument_type =
   | VarArgType
   (** Specific types *)
   | ConstrArgType
-  | OpenConstrArgType
   | ListArgType of argument_type
   | OptArgType of argument_type
   | PairArgType of argument_type * argument_type
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 31125e37c..1fe12ce3e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -231,7 +231,7 @@ GEXTEND Gram
     [ [ id = identref -> id ] ]
   ;
   open_constr:
-    [ [ c = constr -> ((),c) ] ]
+    [ [ c = constr -> c ] ]
   ;
   uconstr:
     [ [ c = constr -> c ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index fdba41385..592c87919 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -219,7 +219,7 @@ module Module :
 
 module Tactic :
   sig
-    val open_constr : open_constr_expr Gram.entry
+    val open_constr : constr_expr Gram.entry
     val constr_with_bindings : constr_expr with_bindings Gram.entry
     val bindings : constr_expr bindings Gram.entry
     val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b98738ce3..6e051a1fc 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -270,7 +270,6 @@ module Make
       | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
       | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
       | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_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
@@ -301,7 +300,6 @@ module Make
       | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
       | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
       | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_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
@@ -331,7 +329,6 @@ module Make
       | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
       | VarArgType -> pr_id (out_gen (topwit wit_var) x)
       | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_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
@@ -1425,6 +1422,12 @@ let () =
     (fun (c,_) -> Printer.pr_glob_constr c)
     Printer.pr_closed_glob
   ;
+  Genprint.register_print0
+    Constrarg.wit_open_constr
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> Printer.pr_glob_constr c)
+    Printer.pr_constr
+  ;
   Genprint.register_print0 Constrarg.wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
     (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 23de87d7d..08d2d21a3 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -727,8 +727,6 @@ and intern_genarg ist x =
     map_raw wit_var intern_hyp ist x
   | ConstrArgType ->
     map_raw wit_constr intern_constr ist x
-  | OpenConstrArgType ->
-    map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x
   | ListArgType _ ->
       let list_unpacker wit l =
         let map x =
@@ -832,6 +830,7 @@ let () =
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
   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);
   Genintern.register_intern0 wit_bindings (lift intern_bindings);
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0ac115d1d..ff6662809 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1120,9 +1120,6 @@ let rec read_match_rule lfun ist env sigma = function
 
 (* misc *)
 
-let mk_open_constr_value ist gl c = 
-  let (sigma,c_interp) = pf_apply (interp_open_constr ist) gl c in
-  sigma, Value.of_constr c_interp
 let mk_hyp_value ist env sigma c =
   (mkVar (interp_hyp ist env sigma c))
 
@@ -1260,10 +1257,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
                                                (Genarg.out_gen (glbwit wit_ident) x)))
           | VarArgType ->
               Ftactic.return (Value.of_constr (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x)))
-          | OpenConstrArgType ->
-              let (sigma,v) =
-                Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (Genarg.out_gen (glbwit wit_open_constr) x))) gl in
-              Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
           | ListArgType VarArgType ->
               let wit = glbwit (wit_list wit_var) in
               let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in
@@ -1626,12 +1619,6 @@ and interp_genarg ist env sigma concl gl x =
       in
       evdref := sigma;
       in_gen (topwit wit_constr) c_interp
-    | OpenConstrArgType ->
-      let expected_type = WithoutTypeConstraint in
-      in_gen (topwit wit_open_constr)
-        (interp_open_constr ~expected_type
-           ist env !evdref
-           (snd (Genarg.out_gen (glbwit wit_open_constr) x)))
     | ListArgType ConstrArgType ->
         let (sigma,v) = interp_genarg_constr_list ist env !evdref x in
 	evdref := sigma;
@@ -2283,6 +2270,7 @@ let () =
   Geninterp.register_interp0 wit_tacvalue (fun ist gl c -> project gl, c);
   Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
   Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
+  Geninterp.register_interp0 wit_open_constr (lifts interp_open_constr);
   Geninterp.register_interp0 wit_bindings interp_bindings';
   Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
   Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index fdf65292a..2132e9a57 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -281,9 +281,6 @@ and subst_genarg subst (x:glob_generic_argument) =
   | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
   | ConstrArgType ->
       in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
-  | OpenConstrArgType ->
-      in_gen (glbwit wit_open_constr)
-        ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x)))
   | ListArgType _ ->
     let list_unpacker wit l =
       let map x =
@@ -322,6 +319,7 @@ let () =
   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);
+  Genintern.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
   Genintern.register_subst0 wit_red_expr subst_redexp;
   Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
   Genintern.register_subst0 wit_bindings subst_bindings;