1. the default for the default equality/absurd/true/false URIs used to be

[helm.git] / components / tactics / discriminationTactics.ml

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 0ffa2c52b4ceb70d0bff28a98a7182e4611c8b60..4c7f5148d1cb5a1ff225c676c7f4ea9931011b01 100644 (file)
--- a/components/tactics/discriminationTactics.ml
+++ b/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