From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 pretyping/arguments_renaming.ml | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'pretyping/arguments_renaming.ml')

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index e18aece0..84295959 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -1,18 +1,23 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
 open Names
 open Globnames
 open Term
+open Constr
 open Environ
 open Util
 open Libobject
+
+module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let name_table =
@@ -37,18 +42,12 @@ let subst_rename_args (subst, (_, (r, names as orig))) =
   let r' = fst (subst_global subst r) in 
   if r==r' then orig else (r', names)
 
-let section_segment_of_reference = function
-  | ConstRef con -> Lib.section_segment_of_constant con
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.LMap.empty, Univ.UContext.empty
-
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
      (try 
-       let vars,_,_ = section_segment_of_reference c in
+       let vars = Lib.variable_section_segment_of_reference c in
        let c' = pop_global_reference c in
-       let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+       let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
@@ -101,7 +100,7 @@ let rename_type_of_constructor env cstruct =
 let rename_typing env c =
   let j = Typeops.infer env c in
   let j' =
-    match kind_of_term c with
+    match kind c with
     | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) }
     | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) }
     | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) }
-- 
cgit v1.2.3