diff options
| author | Talia Ringer | 2019-05-22 16:09:51 -0400 |
|---|---|---|
| committer | Talia Ringer | 2019-05-22 16:09:51 -0400 |
| commit | 577db38704896c75d1db149f6b71052ef47202be (patch) | |
| tree | 946afdb361fc9baaa696df7891d0ddc03a4a8594 /kernel/typeops.ml | |
| parent | 7eefc0b1db614158ed1b322f8c6e5601e3995113 (diff) | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Merge remote-tracking branch 'origin/master' into stm+doc_hook
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 12ffbf4357..af710e7822 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -462,28 +462,6 @@ let type_of_global_in_context env r = let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs -(* Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -let constr_of_global_in_context env r = - let open GlobRef in - match r with - | VarRef id -> mkVar id, Univ.AUContext.empty - | ConstRef c -> - let cb = lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - mkConstU (c, Univ.make_abstract_instance univs), univs - | IndRef ind -> - let (mib,_) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - mkIndU (ind, Univ.make_abstract_instance univs), univs - | ConstructRef cstr -> - let (mib,_) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - mkConstructU (cstr, Univ.make_abstract_instance univs), univs - (************************************************************************) (************************************************************************) |