* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let fake_constructor_tac ~n (proof, goal) =
let module C = Cic in
let module R = CicReduction in
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)