* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug_print = fun _ -> ()
let rec injection_tac ~term =
T.then_
~start:(injection1_tac ~i ~term)
~continuation:(traverse_list (i+1) tl1 tl2)
- | _ -> 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
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
in traverse_list 1 applist1 applist2
| ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
(C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))