diff options
| author | Pierre-Marie Pédrot | 2014-09-08 18:34:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-08 18:46:25 +0200 |
| commit | 7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 (patch) | |
| tree | eeb9435bb4e64566647c5626a2a0f4b83eb58b08 /tactics/tacintern.ml | |
| parent | 7a5eb53973ec3fd921b56339557c48681972849e (diff) | |
Removing the XML plugin.
Left a README, just in case someone will discover the remnants of it
decades from now.
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9d1a9eeaf8..69798a6d20 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -633,7 +633,7 @@ and intern_tactic_seq onlytac ist = function and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with - | TacCall _ | TacExternal _ | Reference _ + | TacCall _ | Reference _ | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> @@ -664,8 +664,6 @@ and intern_tacarg strict onlytac ist = function TacCall (loc, intern_applied_tactic_reference ist f, List.map (intern_tacarg !strict_check false ist) l) - | TacExternal (loc,com,req,la) -> - TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) | TacPretype c -> TacPretype (intern_constr ist c) | TacNumgoals -> TacNumgoals |