From 38e62610be0386a37172fa5aca44e3b3d2c14b9a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Dec 2015 00:09:50 +0100
Subject: Removing dynamic inclusion of constrs in tactic AST.

---
 pretyping/pretyping.ml  | 4 ----
 pretyping/pretyping.mli | 3 ---
 tactics/tacintern.ml    | 2 --
 tactics/tacinterp.ml    | 2 --
 tactics/tacsubst.ml     | 2 --
 5 files changed, 13 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 78f134248c..ce6d189855 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -95,10 +95,6 @@ let search_guard loc env possible_indexes fixdefs =
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
      with Found indexes -> indexes)
 
-(* To embed constr in glob_constr *)
-let ((constr_in : constr -> Dyn.t),
-     (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
-
 (* To force universe name declaration before use *)
 
 let strict_universe_declarations = ref true
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5f0e19cf2b..f8587d01cd 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -148,9 +148,6 @@ val ise_pretype_gen :
 
 (** To embed constr in glob_constr *)
 
-val constr_in : constr -> Dyn.t
-val constr_out : Dyn.t -> constr
-
 val interp_sort : evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 23e7b85a6c..29f679e715 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -711,8 +711,6 @@ and intern_tacarg strict onlytac ist = function
     TacGeneric arg
   | TacDynamic(loc,t) as x ->
     if Dyn.has_tag t "value" then x
-    else if Dyn.has_tag t "constr" then
-      if onlytac then error_tactic_expected loc else x
     else
       let tag = Dyn.tag t in
       anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">")
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 922dc2bc41..bb54a9cb7a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1457,8 +1457,6 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
       let tg = (Dyn.tag t) in
       if String.equal tg "value" then
         Ftactic.return (value_out t)
-      else if String.equal tg "constr" then
-        Ftactic.return (Value.of_constr (constr_out t))
       else
         Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
 	  (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 8e46e625f3..fd7eaafbc6 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -269,8 +269,6 @@ and subst_tacarg subst = function
   | TacDynamic(the_loc,t) as x ->
       (match Dyn.tag t with
 	| "value" -> x
-        | "constr" ->
-          TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
 	| s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
                  (str "Unknown dynamic: <" ++ str s ++ str ">"))
 
-- 
cgit v1.2.3