From 9d65c49f05f946557df4c67b6e752f978e1e9352 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 15:10:50 +0200
Subject: [api] Remove `polymorphic` type alias, use labels instead.

This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
---
 library/lib.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index ae657dbd70..e4054d58cc 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -411,8 +411,8 @@ type abstr_info = {
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
-  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
-		   Decl_kinds.polymorphic * Univ.ContextSet.t)
+  | Variable of (Names.Id.t * Decl_kinds.binding_kind * bool * Univ.ContextSet.t)
+  (** (name, kind, poly, univs) *)
   | Context of Univ.ContextSet.t
 
 let sectab =
@@ -428,12 +428,12 @@ let check_same_poly p vars =
   if List.exists pred vars then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
-let add_section_variable id impl poly ctx =
+let add_section_variable ~name ~kind ~poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
        List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
-       sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+       sectab := (Variable (name,kind,poly,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
@@ -509,11 +509,11 @@ let add_section_replacement f g poly hyps =
     } in
     sectab := (vars,f (inst,args) exps, g info abs) :: sl
 
-let add_section_kn poly kn =
+let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
     add_section_replacement f f poly
 
-let add_section_constant poly kn =
+let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
     add_section_replacement f f poly
 
-- 
cgit v1.2.3


From 5f190f9e12f42a0ff6b5275c8087852a87aff47b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 21 Jun 2019 13:55:03 +0200
Subject: Use named records instead of tuples where `polymorphic` used to be.

Followup on "[api] Remove `polymorphic` type alias, use labels instead."
---
 library/lib.ml | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index e4054d58cc..3eb74808e4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -411,8 +411,12 @@ type abstr_info = {
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
-  | Variable of (Names.Id.t * Decl_kinds.binding_kind * bool * Univ.ContextSet.t)
-  (** (name, kind, poly, univs) *)
+  | Variable of {
+      id:Names.Id.t;
+      kind:Decl_kinds.binding_kind;
+      poly:bool;
+      univs:Univ.ContextSet.t;
+    }
   | Context of Univ.ContextSet.t
 
 let sectab =
@@ -424,16 +428,16 @@ let add_section () =
                 (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
 let check_same_poly p vars =
-  let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+  let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
   if List.exists pred vars then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
-let add_section_variable ~name ~kind ~poly ctx =
+let add_section_variable ~name ~kind ~poly univs =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
        List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
-       sectab := (Variable (name,kind,poly,ctx)::vars,repl,abs)::sl
+       sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
@@ -448,7 +452,7 @@ let is_polymorphic_univ u =
     let open Univ in
     List.iter (fun (vars,_,_) ->
         List.iter (function
-            | Variable (_,_,poly,(univs,_)) ->
+            | Variable {poly;univs=(univs,_)} ->
               if LSet.mem u univs then raise (PolyFound poly)
             | Context (univs,_) ->
               if LSet.mem u univs then raise (PolyFound true)
@@ -459,12 +463,12 @@ let is_polymorphic_univ u =
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
-      (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | (Variable (_,_,poly,ctx)::idl,hyps) ->
+      (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
+    | (Variable {poly;univs}::idl,hyps) ->
         let l, r = aux (idl,hyps) in
-          l, if poly then Univ.ContextSet.union r ctx else r
+          l, if poly then Univ.ContextSet.union r univs else r
     | (Context ctx :: idl, hyps) ->
        let l, r = aux (idl, hyps) in
        l, Univ.ContextSet.union r ctx
@@ -543,7 +547,7 @@ let variable_section_segment_of_reference gr =
 let section_instance = function
   | VarRef id ->
      let eq = function
-       | Variable (id',_,_,_) -> Names.Id.equal id id'
+       | Variable {id=id'} -> Names.Id.equal id id'
        | Context _ -> false
      in
      if List.exists eq (pi1 (List.hd !sectab))
-- 
cgit v1.2.3