diff options
| author | Matthieu Sozeau | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /plugins/funind | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a3af23dcda..f0c7b5a7f7 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -964,7 +964,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = 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 = decompose_prod_n_assum (nb_params + nb_args) - ((*FIXME*)f_def.const_type) in + (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)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 eqn type_ctxt in let f_id = Label.to_id (con_label (fst (destConst f))) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d6ad5575b0..49f8335908 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -771,7 +771,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env body, Constrextern.extern_type false env - ((*FIXNE*) c_body.const_type) + ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) ) ) () diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index d0497f6f6c..2e524a35f0 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -139,7 +139,7 @@ let showind (id:Id.t) = print_string (string_of_name nm^":"); prconstr tp; print_string "\n") ib1.mind_arity_ctxt; - Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity; + Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) ib1.mind_user_lc |