diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 20:02:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 23:39:01 +0200 |
| commit | 7002b3daca6da29eadf80019847630b8583c3daf (patch) | |
| tree | 9dcc3b618d33dd416805f70e878d71d007ddf4ff /pretyping/arguments_renaming.ml | |
| parent | 5de89439d459edd402328a1e437be4d8cd2e4f46 (diff) | |
Move to a representation of universe polymorphic constants using indices for variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
Diffstat (limited to 'pretyping/arguments_renaming.ml')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index be22030ce..3c7d4f75b 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -41,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.UContext.empty + | _ -> [], 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 |