diff options
| author | herbelin | 2006-10-28 19:35:09 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-28 19:35:09 +0000 |
| commit | 359e4ffe307d7d8dd250735373fc6354a58ecff5 (patch) | |
| tree | 7204cb80cb272118a7ee60e9790d91d0efd11894 /library | |
| parent | 8bcd34ae13010797a974b0f3c16df6e23f2cb254 (diff) | |
Extension du polymorphisme de sorte au cas des définitions dans Type.
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/impargs.ml | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/library/global.ml b/library/global.ml index 19b4165199..30281bcc70 100644 --- a/library/global.ml +++ b/library/global.ml @@ -141,10 +141,10 @@ open Libnames let type_of_reference env = function | VarRef id -> Environ.named_type id env - | ConstRef c -> Environ.constant_type env c + | ConstRef c -> Typeops.type_of_constant env c | IndRef ind -> let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif | ConstructRef cstr -> let specif = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in diff --git a/library/impargs.ml b/library/impargs.ml index ffdeb0b88d..b5488031bf 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -259,10 +259,9 @@ let list_of_implicits = function let constants_table = ref Cmap.empty -let compute_constant_implicits kn = +let compute_constant_implicits cst = let env = Global.env () in - let cb = lookup_constant kn env in - auto_implicits env (body_of_type cb.const_type) + auto_implicits env (Typeops.type_of_constant env cst) let constant_implicits sp = try Cmap.find sp !constants_table with Not_found -> No_impl @@ -282,12 +281,13 @@ let compute_mib_implicits kn = let ar = Array.to_list (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip))) + (fun mip -> + (Name mip.mind_typename, None, type_of_inductive env (mib,mip))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = type_of_inductive (mib,mip) in + let ar = type_of_inductive env (mib,mip) in ((IndRef ind,auto_implicits env ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) mip.mind_nf_lc) |