From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 pretyping/arguments_renaming.ml | 50 +++++++++++++++++------------------------
 1 file changed, 20 insertions(+), 30 deletions(-)

(limited to 'pretyping/arguments_renaming.ml')

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 78290e03..3cfc0dc8 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,32 +8,20 @@
 
 (*i*)
 open Names
-open Libnames
-open Decl_kinds
+open Globnames
 open Term
-open Sign
-open Evd
 open Environ
-open Nametab
-open Mod_subst
 open Util
-open Pp
 open Libobject
-open Nameops
 (*i*)
 
-let empty_name_table = (Refmap.empty : name list list Refmap.t)
-let name_table = ref empty_name_table
-
-let _ =
-  Summary.declare_summary "rename-arguments"
-    { Summary.freeze_function = (fun () -> !name_table);
-      Summary.unfreeze_function = (fun r -> name_table := r);
-      Summary.init_function = (fun () -> name_table := empty_name_table) }
+let name_table =
+  Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+    ~name:"rename-arguments"
 
 type req =
   | ReqLocal
-  | ReqGlobal of global_reference * name list list
+  | ReqGlobal of global_reference * Name.t list list
 
 let load_rename_args _ (_, (_, (r, names))) =
   name_table := Refmap.add r names !name_table
@@ -53,12 +41,12 @@ 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,_,_ = 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 names' = List.map (fun l -> var_names @ l) names in
@@ -99,22 +87,24 @@ let rename_type ty ref =
   with Not_found -> ty
 
 let rename_type_of_constant env c =
-  let ty = Typeops.type_of_constant env c in
-  rename_type ty (ConstRef c)
+  let ty = Typeops.type_of_constant_in env c in
+  rename_type ty (ConstRef (fst c))
 
 let rename_type_of_inductive env ind =
   let ty = Inductiveops.type_of_inductive env ind in
-  rename_type ty (IndRef ind)
+  rename_type ty (IndRef (fst ind))
 
 let rename_type_of_constructor env cstruct =
   let ty = Inductiveops.type_of_constructor env cstruct in
-  rename_type ty (ConstructRef cstruct)
+  rename_type ty (ConstructRef (fst cstruct))
 
 let rename_typing env c =
-  let j = Typeops.typing env c in
-  match kind_of_term c with
-  | Const c -> { j with uj_type = rename_type j.uj_type (ConstRef c) }
-  | Ind i -> { j with uj_type = rename_type j.uj_type (IndRef i) }
-  | Construct k -> { j with uj_type = rename_type j.uj_type (ConstructRef k) }
-  | _ -> j
+  let j = Typeops.infer env c in
+  let j' =
+    match kind_of_term 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) }
+    | _ -> j
+  in j'
 
-- 
cgit v1.2.3