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.

7 files changed, 16 insertions, 43 deletions

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