diff options
| author | filliatr | 2000-01-21 18:42:22 +0000 |
|---|---|---|
| committer | filliatr | 2000-01-21 18:42:22 +0000 |
| commit | 40183da6b54d8deef242bac074079617d4a657c2 (patch) | |
| tree | 4e70870a5b1e36ba65965f6e87cd8141d01d8d75 /kernel/typeops.ml | |
| parent | 249c6b5e1e2d00549dde9093e134df2f25a68609 (diff) | |
gros commit de tout ce que j'ai fait pendant les vacances :
- tactics/Equality
- debug du discharge
- constr_of_compattern implante vite fait / mal fait en attendant mieux
- theories/Logic (ne passe pas entierrement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1254d5ef99..4b20f3b0a9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -84,7 +84,7 @@ let check_hyps id env sigma hyps = let type_of_constant env sigma (sp,args) = let cb = lookup_constant sp env in let hyps = cb.const_hyps in - check_hyps (basename sp) env sigma hyps; + (* TODO: check args *) instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) (* Inductive types. *) @@ -99,7 +99,7 @@ let instantiate_arity mis = let type_of_inductive env sigma i = let mis = lookup_mind_specif i env in let hyps = mis.mis_mib.mind_hyps in - check_hyps (basename mis.mis_sp) env sigma hyps; + (* TODO: check args *) instantiate_arity mis (* Constructors. *) @@ -112,7 +112,7 @@ let instantiate_lc mis = let type_of_constructor env sigma ((ind_sp,j),args as cstr) = let mind = inductive_of_constructor cstr in let mis = lookup_mind_specif mind env in - check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps); + (* TODO: check args *) let specif = instantiate_lc mis in let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in if j > mis_nconstr mis then @@ -161,7 +161,7 @@ let type_of_existential env sigma c = let evi = Evd.map sigma ev in let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in - check_hyps id env sigma hyps; + (* TODO: check args *) instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) |