aboutsummaryrefslogtreecommitdiff
path: root/kernel/declarations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/declarations.ml')
-rw-r--r--kernel/declarations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4f98bb8b07..c7f8087428 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -71,7 +71,7 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
type recarg =
| Norec
- | Mrec of int
+ | Mrec of inductive
| Imbr of inductive
let subst_recarg sub r = match r with