diff options
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 2b4b6245a..e98a0952b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = let new_env = add_pat_variables env pat typ in let res = fst ( - Sign.fold_rel_context + Context.fold_rel_context (fun (na,v,t) (env,ctxt) -> match na with | Anonymous -> assert false |