From aa29c92dfa395e2f369e81bd72cef482cdf90c65 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 20 Sep 2016 09:11:09 +0200
Subject: Stylistic improvements in intf/decl_kinds.mli.

We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.

The previously common idom:

if pi2 kind (* polymorphic *) then ... else ...

becomes:

if kind.polymorphic then ... else ...

To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
---
 tactics/leminv.ml  | 2 +-
 tactics/tactics.ml | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d80e862418..c7b8e6cc05 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -233,7 +233,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
+  let entry = definition_entry ~polymorphic:(Flags.use_polymorphic_flag ())
 			       ~univs:(snd ctx) invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9d0e9f0842..86c0b9dd5c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4888,7 +4888,9 @@ let anon_id = Id.of_string "anonymous"
 
 let tclABSTRACT name_op tac =
   let open Proof_global in
-  let default_gk = (Global, false, Proof Theorem) in
+  let default_gk =
+    { locality = Global; polymorphic = false; object_kind = Proof Theorem }
+  in
   let s, gk = match name_op with
     | Some s ->
       (try let _, gk, _ = current_proof_statement () in s, gk
-- 
cgit v1.2.3