diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
3 files changed, 0 insertions, 6 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 23e7b85a6..29f679e71 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 922dc2bc4..bb54a9cb7 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 8e46e625f..fd7eaafbc 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 ">")) |