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.

3 files changed, 6 insertions, 9 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d55d6ce6ba..86c2b7a573 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -147,10 +147,7 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let default_goal_kind =
-  { locality = Global; polymorphic = false; object_kind = Proof Theorem }
-
-let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ tac =
+let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   start_proof id goal_kind evd sign typ terminator;
@@ -164,10 +161,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ ta
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env ctx ?(polymorphic=false) typ tac =
+let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = { locality = Global; polymorphic; object_kind = Proof Theorem } in
+  let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index aa01969b77..f2f4b11ed3 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -169,7 +169,7 @@ val build_constant_by_tactic :
   types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 911d4ffbc1..2956d623fd 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
-  let poly = strength.Decl_kinds.polymorphic in
+  let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
@@ -398,7 +398,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
- let { pid; proof; strength = { Decl_kinds.polymorphic }} = cur_pstate () in
+ let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in