diff options
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index eae72d9e8..a7481370a 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -579,8 +579,8 @@ let ids_of_pat = ids_of_pat Id.Set.empty let id_of_name = function - | Names.Anonymous -> Id.of_string "x" - | Names.Name x -> x + | Anonymous -> Id.of_string "x" + | Name x -> x (* TODO: finish Rec caes *) let ids_of_glob_constr c = |