X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdiscriminationTactics.ml;h=4c7f5148d1cb5a1ff225c676c7f4ea9931011b01;hb=2957d67b2b74224cf3bb768461d60f07062e1b9d;hp=0ffa2c52b4ceb70d0bff28a98a7182e4611c8b60;hpb=8c19127e7ee6c71006838f89583a3283451b664c;p=helm.git

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 0ffa2c52b..4c7f5148d 100644
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -206,6 +206,14 @@ let discriminate'_tac ~term =
  let module U = UriManager in
  let module P = PrimitiveTactics in
  let module T = Tacticals in
+ let true_URI =
+  match LibraryObjects.true_URI () with
+     Some uri -> uri
+   | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
+ let false_URI =
+  match LibraryObjects.false_URI () with
+     Some uri -> uri
+   | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
  let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
  let find_discriminating_consno t1 t2 =
    let rec aux t1 t2 =
@@ -259,8 +267,8 @@ let discriminate'_tac ~term =
                   C.Lambda (binder, source, (aux target (k+1)))
               | _ -> 
                   if (id = false_constr_id)
-                  then (C.MutInd(LibraryObjects.false_URI (),0,[]))
-                  else (C.MutInd(LibraryObjects.true_URI (),0,[]))
+                  then (C.MutInd(false_URI,0,[]))
+                  else (C.MutInd(true_URI,0,[]))
             in
             (CicSubstitution.lift 1 (aux red_ty 1)))
           constructor_list
@@ -294,7 +302,7 @@ let discriminate'_tac ~term =
       let (proof',goals') = 
         ProofEngineTypes.apply_tactic 
           (EliminationTactics.elim_type_tac
-            (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+            (C.MutInd (false_URI, 0, [])))
           status 
       in
       (match goals' with