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/functional_principles_proofs.ml | 2 +- plugins/funind/functional_principles_types.ml | 7 ++----- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/indfun.ml | 4 ++-- plugins/funind/invfun.ml | 4 ++-- 5 files changed, 8 insertions(+), 11 deletions(-) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index d4e410bd69..651895aa08 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1004,7 +1004,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d57b931785..d1e7d8a5a8 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) hook @@ -359,10 +359,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = - let poly = Flags.is_universe_polymorphism () in - Evd.const_univ_entry ~poly evd' - in + let univs = Evd.const_univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7c80b776a4..98aaa081c3 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1494,7 +1494,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> 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},_),_,_,_,_),_) -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 96eb7fbc60..d1a227d517 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -804,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) + (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd typ (Lemmas.mk_hook (fun _ _ -> ())); @@ -866,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by -- cgit v1.2.3