X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=b1727fb7d401d35fa761a2dd9c4cbb3540c9bf6e;hb=abd976fb6603a85c1da6d1582114e7c1fa472449;hp=cca2c1a5902b9256736dd8b1001abe42c1d3ea22;hpb=3cc1aec78e4c51aa766127487f19a3d38a4b56ae;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index cca2c1a59..b1727fb7d 100644
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -206,6 +206,11 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let uri,metasenv,pbo,pty = proof in
   let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   assert (hyps_pat = []); (*CSC: not implemented yet *)
+  let eq_URI =
+   match LibraryObjects.eq_URI () with
+      Some uri -> uri
+    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
+  in
   let context_len = List.length context in
   let subst,metasenv,u,_,selected_terms_with_context =
    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
@@ -269,7 +274,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
             ~start:(
               P.cut_tac 
                (C.Appl [
-                 (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ;
+                 (C.MutInd (eq_URI, 0, [])) ;
                  ty_of_with_what ; 
                  what ; 
                  with_what]))