diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2a66ba8523..0a288c76e1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -86,7 +86,9 @@ let def_of_const t = let type_of_const sigma t = match (EConstr.kind sigma t) with - Const sp -> Typeops.type_of_constant (Global.env()) sp + | Const sp -> + (* FIXME discarding universe constraints *) + Typeops.type_of_constant_in (Global.env()) sp |_ -> assert false let constr_of_global x = @@ -1449,7 +1451,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in let terminate_constr = EConstr.of_constr terminate_constr in - let nargs = nb_prod (project g) (EConstr.of_constr (fst (type_of_const sigma terminate_constr))) (*FIXME*) in + let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; |