aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/rawterm_to_relation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index e6b3ba3ec..7d0d134c5 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -446,7 +446,7 @@ let rec pattern_to_term_and_type env typ = function
let patl_as_term =
List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl
in
- mkRApp(mkRRef(Libnames.ConstructRef constr),
+ mkRApp(mkRRef(ConstructRef constr),
implicit_args@patl_as_term
)