T.then_
~start:(injection1_tac ~i ~term)
~continuation:(traverse_list (i+1) tl1 tl2)
- | _ -> raise (ProofEngineTypes.Fail "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???") ; T.id_tac
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) ; T.id_tac
in traverse_list 1 applist1 applist2
| ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
(C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
(* raise (ProofEngineTypes.Fail "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac
| _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac
)
- | _ -> raise (ProofEngineTypes.Fail "Injection: not a projectable equality")
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
)
- | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation")
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
) status
in
ProofEngineTypes.mk_tactic (injection_tac ~term)
in aux reduced_cty 1
)
constructor_list
- | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible"))
in
ProofEngineTypes.apply_tactic
(T.thens
match gty with
(C.Appl (C.MutInd (_,_,_)::arglist)) ->
List.nth arglist 1
- | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct"))
in
ProofEngineTypes.apply_tactic
(ReductionTactics.change_tac
)
])
status
- | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality"))
)
- | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not an equality"))
in
ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
;;
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
- let fail msg = raise (ProofEngineTypes.Fail ("Discriminate: " ^ msg)) in
+ let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
let find_discriminating_consno t1 t2 =
let rec aux t1 t2 =
match t1, t2 with