diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 35952c9dd..f68f75359 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -43,10 +43,6 @@ let error_syntactic_metavariables_not_allowed loc = let error_tactic_expected loc = user_err_loc (loc,"",str "Tactic expected.") -let skip_metaid = function - | AI x -> x - | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc - (** Generic arguments *) type glob_sign = Genintern.glob_sign = { |