From 30a908becf31d91592a1f7934cfa3df2d67d1834 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Sep 2016 17:11:12 +0200 Subject: Revert "Merge remote-tracking branch 'github/pr/283' into trunk" I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb. --- plugins/derive/derive.ml | 5 +---- plugins/funind/functional_principles_proofs.ml | 4 +--- plugins/funind/functional_principles_types.ml | 8 ++------ plugins/funind/indfun.ml | 4 +--- plugins/funind/indfun_common.ml | 7 +++---- plugins/funind/invfun.ml | 15 +++++---------- plugins/funind/recdef.ml | 16 +++------------- 7 files changed, 16 insertions(+), 43 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 12fd8359a..e39d17b52 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -22,10 +22,7 @@ let start_deriving f suchthat lemma = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.{ locality = Global; - polymorphic = false; - object_kind = DefinitionBody Definition } - in + let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in (** create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bba7b3c59..527f4f0b1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -996,9 +996,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.{ locality = Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Proof Theorem } + (Decl_kinds.Global, Flags.is_universe_polymorphism (), (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 4f5f167c2..cc699e5d3 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -288,9 +288,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin begin Lemmas.start_proof new_princ_name - Decl_kinds.{ locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Proof Decl_kinds.Theorem } + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd new_principle_type hook @@ -341,9 +339,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' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~polymorphic:(Flags.is_universe_polymorphism ()) - ~univs:(snd (Evd.universe_context evd')) value - in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( Declare.declare_constant name diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index efbc1507f..99b04898b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -395,9 +395,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in Command.do_definition fname - { locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Definition } pl + (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8c6673732..a45effb16 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -148,18 +148,17 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const goal_kind hook = +let save with_clean id const (locality,_,kind) hook = let fix_exn = Future.fix_exn_of const.const_entry_body in - let locality = goal_kind.locality in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> - let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in + let k = Kindops.logical_kind_of_goal_kind kind in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) | Discharge | Local | Global -> let local = get_locality locality in - let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in + let k = Kindops.logical_kind_of_goal_kind kind in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 6d042b3a4..c8b4e4833 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -832,9 +832,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - Decl_kinds.{ locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Proof Decl_kinds.Theorem } + (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) !evd typ (Lemmas.mk_hook (fun _ _ -> ())); @@ -895,13 +893,10 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - Lemmas.start_proof lem_id - Decl_kinds.{ locality = Decl_kinds.Global; - polymorphic = Flags.is_universe_polymorphism (); - object_kind = Decl_kinds.Proof Decl_kinds.Theorem } - sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + Lemmas.start_proof lem_id + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + (fst lemmas_types_infos.(i)) + (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 75495ed98..f43251bc5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1348,9 +1348,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in Lemmas.start_proof na - { locality = Decl_kinds.Global; - polymorphic = false (* FIXME *); - object_kind = Decl_kinds.Proof Decl_kinds.Lemma } + (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () @@ -1396,12 +1394,8 @@ let com_terminate hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in - let goal_kind = { locality = Global; - polymorphic = false; (* FIXME *) - object_kind = Proof Lemma } - in Lemmas.start_proof thm_name - goal_kind ~sign:(Environ.named_context_val env) + (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (compute_terminate_type nb_args fonctional_ref) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); @@ -1451,11 +1445,7 @@ let (com_eqn : int -> Id.t -> let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let goal_kind = { locality = Global; - polymorphic = false; - object_kind = Proof Lemma } - in - (Lemmas.start_proof eq_name goal_kind + (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) evmap equation_lemma_type -- cgit v1.2.3