diff options
Diffstat (limited to 'pretyping/arguments_renaming.ml')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 50 |
1 files changed, 20 insertions, 30 deletions
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' |