diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-03 20:30:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-03 20:33:47 +0100 |
| commit | 3e0643a4073c02767f44c0b77019a0e183e1e296 (patch) | |
| tree | 9a10db752c2ce810da1684defbb83d99af209075 /tactics/tacsubst.ml | |
| parent | f135a3967ca3d22bdc5566a54f042ba5bd6a343c (diff) | |
Removing the globTacticIn primitive.
It was not used in Coq codebase, and the only known user was ssreflect up
to commit 95354e0dee.
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index afffaffbe..8e46e625f 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -268,7 +268,7 @@ and subst_tacarg subst = function | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> (match Dyn.tag t with - | "tactic" | "value" -> x + | "value" -> x | "constr" -> TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t))) | s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp" |