X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=5186345b661ad58a8355be382e3ca589cc1309ef;hb=13049dd275c7cb45b003f5860f1a400a66e37b06;hp=8d07811ea3333d450caf68f347e39f1b6a1772e6;hpb=b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 8d07811ea..5186345b6 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -522,7 +522,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let status,_ =
   List.fold_right2
    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
-     assert (id1=id2);
+     assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
      match e1,e2 with
         `Decl t1, NCic.Decl t2 ->
           let status = eq status ctx t1 t2 in