diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 15:04:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 15:37:34 +0100 |
| commit | 098d283e58966124cfe0e97a3229a9e7e6284120 (patch) | |
| tree | 9ffc61382b3b66a6da24276fd15b14175f21e887 /tactics | |
| parent | d5656a6c28f79d59590d4fde60c5158a649d1b65 (diff) | |
Removing the UConstr entry of the tactic_arg AST.
This was redundant with the wit_uconstr generic argument, so there was no real
point on keeping it there.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
3 files changed, 1 insertions, 8 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index a069fd755..89dc843cb 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -651,7 +651,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacCall _ | Reference _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a - | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> + | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) and intern_tactic_or_tacarg ist = intern_tactic false ist @@ -665,7 +665,6 @@ and intern_tactic_fun ist (var,body) = and intern_tacarg strict onlytac ist = function | Reference r -> intern_non_tactic_reference strict ist r | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) - | UConstr c -> UConstr (intern_constr ist c) | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f | TacCall (loc,f,l) -> TacCall (loc, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1a8a95158..bf5f9ddc8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1365,11 +1365,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) end } - | UConstr c -> - Ftactic.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - Ftactic.return (Value.of_uconstr (interp_uconstr ist env c)) - end } | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist r | TacCall (loc,f,l) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 3f103a290..55941c1ca 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -247,7 +247,6 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | UConstr c -> UConstr (subst_glob_constr subst c) | TacCall (_loc,f,l) -> TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) | TacFreshId _ as x -> x |