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