- PrimitiveTactics.apply_tac
- ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
- ~status:(proof, goal)
- | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
+ ProofEngineTypes.apply_tactic (
+ PrimitiveTactics.apply_tac
+ ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)))
+ (proof, goal)
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Constructor: failed"))