diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 5e686c41e..14071d869 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -658,6 +658,7 @@ let make_bl_scheme mode mind = let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in + let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in @@ -783,6 +784,7 @@ let make_lb_scheme mode mind = let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.make_evar_universe_context (Global.env ()) None in let side_eff = side_effect_of_mode mode in + let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in @@ -956,7 +958,7 @@ let make_eq_decidability mode mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx - (compute_dec_goal (ind,u) lnamesparrec nparrec) + (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) (compute_dec_tact ind lnamesparrec nparrec) in ([|ans|], ctx), Safe_typing.empty_private_constants |