From c643a4c20b033c27b153d186128093791b687b77 Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Thu, 30 Mar 2017 17:24:45 +0200 Subject: solving implicit resolution in Function --- plugins/funind/glob_term_to_relation.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'plugins/funind/glob_term_to_relation.ml') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 68e097fe9..8c0b28ae8 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1288,17 +1288,20 @@ let do_build_inductive let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) - (* try *) - (* Typing.e_type_of env evd (mkConstU c) *) - (* with Not_found -> *) - (* raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *) env ) funnames (Array.of_list funconstants) (evd,Global.env ()) in - let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + (* we solve and replace the implicits *) + let rta = + Array.mapi (fun i rt -> + let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in + resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt + ) rta + in + let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = -- cgit v1.2.3