From 8a35d93061c67dcdbb12337b78fcb35d72957f51 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:33 +0200
Subject: Minor cosmetic commit.

---
 vernac/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index 6eb7037f84..f31fce8859 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1155,7 +1155,7 @@ let interp_fixpoint l ntns =
 
 let interp_cofixpoint l ntns =
   let (env,_,pl,evd),fix,info = interp_recursive false l ntns in
-  check_recursive false  env evd fix;
+  check_recursive false env evd fix;
   (fix,pl,Evd.evar_universe_context evd,info)
     
 let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-- 
cgit v1.2.3