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.

3 files changed, 3 insertions, 18 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 23de87d7db..08d2d21a3f 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 0ac115d1d5..ff66628098 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 fdf65292a1..2132e9a573 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;