aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r--plugins/funind/recdef.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6b63d7771..4fd9e0ff8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -693,7 +693,7 @@ let mkDestructEq :
(fun g2 ->
let changefun patvars = { run = fun sigma ->
let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
- redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
+ redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
} in
Proofview.V82.of_tactic (change_in_concl None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
- let eq' = nf_zeta env_eq' eq' in
+ let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
let res =
(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)