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