diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9e4060752..6b06a0534 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -124,7 +124,7 @@ let lookup_ltacref r = KNmap.find r !mactab let find_ident id ist = Id.Set.mem id ist.ltacvars || - List.mem id (ids_of_named_context (Environ.named_context ist.genv)) + Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv)) let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars @@ -138,7 +138,7 @@ let find_ctxvar id ist = Id.Set.mem id ist.ltacvars let find_ltacvar id ist = Id.Set.mem id ist.ltacvars let find_hyp id ist = - List.mem id (ids_of_named_context (Environ.named_context ist.genv)) + Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv)) (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *) (* be fresh in which case it is binding later on *) |