aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/modops.ml')
-rw-r--r--checker/modops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/modops.ml b/checker/modops.ml
index e6428d5ab..f5d54c361 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -85,7 +85,7 @@ let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
let con = constant_of_kn kn in
- let mind = mind_of_kn kn in
+ let mind = mind_of_delta resolver (mind_of_kn kn) in
match elem with
| SFBconst cb ->
(* let con = constant_of_delta resolver con in*)