From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 16 Apr 2009 12:23:22 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4078
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13049dd275c7cb45b003f5860f1a400a66e37b06;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