diff options
| author | ppedrot | 2013-08-28 07:44:10 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-28 07:44:10 +0000 |
| commit | 90a73b08da2fe80b0298997f1f9adb65afdfbf54 (patch) | |
| tree | a3d0afeadbadfb7f3ecfc5a0df0de89c5c07a3af /tactics | |
| parent | 3d35bfd5b25c6a37ab9d1cf62b51b4d718553f59 (diff) | |
Removing some lone List.assoc & List.mem in lib.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 21 |
1 files changed, 6 insertions, 15 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 29eb9e9ec8..033f460623 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -775,21 +775,12 @@ let add_transparency l b local dbnames = dbnames let add_extern pri pat tacast local dbname = - (* We check that all metas that appear in tacast have at least - one occurence in the left pattern pat *) - let tacmetas = [] in - match pat with - | Some (patmetas,pat) -> - (match (List.subtract tacmetas patmetas) with - | i::_ -> - errorlabstrm "add_extern" - (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.") - | [] -> - Lib.add_anonymous_leaf - (inAutoHint(local,dbname, AddHints [make_extern pri (Some pat) tacast]))) - | None -> - Lib.add_anonymous_leaf - (inAutoHint(local,dbname, AddHints [make_extern pri None tacast])) + let pat = match pat with + | None -> None + | Some (_, pat) -> Some pat + in + let hint = local, dbname, AddHints [make_extern pri pat tacast] in + Lib.add_anonymous_leaf (inAutoHint hint) let add_externs pri pat tacast local dbnames = List.iter (add_extern pri pat tacast local) dbnames |