From 0fa0ad02cb17a19edcd81efc8e41ccdd4f37ffaf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 11 Oct 2018 16:23:14 +0200
Subject: Remove is_universe_polymorphism in funind

Funind doesn't support polymorphism.
---
 plugins/funind/indfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/indfun.ml')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9a6169d42a..35acbea488 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -414,7 +414,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       ComDefinition.do_definition
         ~program_mode:false
 	fname
-	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
+        (Decl_kinds.Global,false,Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
@@ -431,7 +431,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
-- 
cgit v1.2.3