...

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 8d07811ea3333d450caf68f347e39f1b6a1772e6..5186345b661ad58a8355be382e3ca589cc1309ef 100644 (file)
--- 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