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 0ed800626d762480895d176fefd9020e3a6b9493..722e36740a8a570a7248e9e75e54803d2f12cde2 100644 (file)
--- 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) *)