From 9903b47cdccc2fe98a905ab085cb24ca36de1aed Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Apr 2017 11:12:26 +0200
Subject: Disable debug printing

Fix a mistake in record declaration
---
 vernac/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index 8a83dceeff..b95131b724 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -584,7 +584,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure Finite cum poly (Universes.univ_inf_ind_from_universe_context ctx) idstruc
+	let ind = declare_structure finite cum poly (Universes.univ_inf_ind_from_universe_context ctx) idstruc
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
-- 
cgit v1.2.3