From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jul 2011 15:02:24 +0000 (+0000)
Subject: The name of the constructor for jmeq changed.
X-Git-Tag: make_still_working~2365
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e6b9fe97056bdffc515e1951de67d85d40e964c;p=helm.git

The name of the constructor for jmeq changed.
---

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index 0ed800626..722e36740 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -272,7 +272,7 @@ let discriminate_tac ~context cur_eq status =
   pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq)));
 
   let dbranch it ~use_jmeq leftno consno =
-    let refl_id = mk_id (if use_jmeq then "refl_jmeq" else "refl") in
+    let refl_id = mk_id (if use_jmeq then "jmrefl" else "refl") in
     pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
     let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
     (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)