From b341b58104ff14f10a5e170d4bfbc7a02f12755f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Mar 2020 02:43:42 -0400
Subject: [record] Cleanup of data structure and functions [1/2]

In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.

The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.
---
 vernac/vernacentries.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'vernac/vernacentries.ml')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 824bf35b1d..6a09250627 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -715,16 +715,16 @@ let should_treat_as_uniform () =
   else ComInductive.NonUniformParameters
 
 let vernac_record ~template udecl ~cumulative k ~poly finite records =
-  let map ((coe, id), binders, sort, nameopt, cfs) =
-    let const = match nameopt with
-    | None -> Nameops.add_prefix "Build_" id.v
+  let map ((is_coercion, name), binders, sort, nameopt, cfs) =
+    let idbuild = match nameopt with
+    | None -> Nameops.add_prefix "Build_" name.v
     | Some lid ->
       let () = Dumpglob.dump_definition lid false "constr" in
       lid.v
     in
     let () =
       if Dumpglob.dump () then
-        let () = Dumpglob.dump_definition id false "rec" in
+        let () = Dumpglob.dump_definition name false "rec" in
         let iter (x, _) = match x with
         | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
           Dumpglob.dump_definition (make ?loc id) false "proj"
@@ -732,7 +732,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records =
         in
         List.iter iter cfs
     in
-    coe, id, binders, cfs, const, sort
+    Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort }
   in
   let records = List.map map records in
   ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records)
-- 
cgit v1.2.3