From 1923e2a87e8754e63e8d9edcdfe178a841ff96d2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 Oct 2019 21:06:54 +0200
Subject: [inductive] [declare] Move full inductive declaration to declareInd

Patch suggested by Gaëtan Gilbert
---
 vernac/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/record.ml')

diff --git a/vernac/record.ml b/vernac/record.ml
index 831fb53549..b60bfdfa22 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -466,7 +466,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   in
   let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
   let impls = List.map (fun _ -> paramimpls, []) record_data in
-  let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
+  let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
       ~primitive_expected:!primitive_flag
   in
   let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
-- 
cgit v1.2.3