diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index c4fa51c4b..3976fcf14 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -351,8 +351,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = ))) ) in - Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> - let type_of_pq = type_of p in + Tacmach.New.of_old (fun gl -> pf_type_of gl p) >>= fun type_of_pq -> let u,v = destruct_ind type_of_pq in let lb_type_of_p = try @@ -412,6 +411,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> + begin try (* type_of can raise an exception *) let tt1 = type_of t1 in if eq_constr t1 t2 then aux q1 q2 else ( @@ -452,6 +452,8 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt = aux q1 q2 ] ) ) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end | ([],[]) -> Proofview.tclUNIT () | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity.")) in |