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 /contrib/funind | |
| 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 'contrib/funind')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 3 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 6 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 2 |
3 files changed, 6 insertions, 5 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index ab411cf11d..14e2233fe8 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -890,7 +890,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) - let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) f_def.const_type in + let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) + (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in let f_id = id_of_label (con_label (destConst f)) in diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index c7f100c365..82bb286953 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -306,8 +306,7 @@ let generate_principle list_map_i (fun i x -> let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in - let princ_type = - (Global.lookup_constant princ).Declarations.const_type + let princ_type = Typeops.type_of_constant (Global.env()) princ in Functional_principles_types.generate_functional_principle interactive_proof @@ -682,7 +681,8 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env body, - Constrextern.extern_type false env c_body.const_type + Constrextern.extern_type false env + (Typeops.type_of_constant_type env c_body.const_type) ) ) () diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 40c90f5a1b..04110ea989 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -101,7 +101,7 @@ let id_to_constr id = let generate_type g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) - let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph)) in + let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with |