diff options
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 7b758da8e8..d36d86a65b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -375,7 +375,7 @@ let rec pattern_to_term pt = DAst.with_val (function let patl_as_term = List.map pattern_to_term patternl in - mkGApp(mkGRef(Globnames.ConstructRef constr), + mkGApp(mkGRef(GlobRef.ConstructRef constr), implicit_args@patl_as_term ) ) pt |