All the tactics have been ported to use the objects in LibraryObjects.

diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml
index d9fb88f6bf1b9cd9e41bcbbb35a7c84288cb0361..f7613fe1949789b496cc7820d583d3d774c91620 100644 (file)
--- a/helm/ocaml/cic/libraryObjects.ml
+++ b/helm/ocaml/cic/libraryObjects.ml
@@ -57,3 +57,7 @@ let trans_eq_URI =
  something_URI
   HelmLibraryObjects.Logic.trans_eq_URI
   MatitaLibraryObjects.Equality.trans_eq_URI
+
+let true_URI = MatitaLibraryObjects.Logic.true_URI
+let false_URI = MatitaLibraryObjects.Logic.false_URI
+let absurd_URI = MatitaLibraryObjects.Logic.absurd_URI

diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli
index 6a7bb1833dc11469aec411b6e39a2c827f2ba325..859b4e732daf302b55d945e955afb4d152696ed5 100644 (file)
--- a/helm/ocaml/cic/libraryObjects.mli
+++ b/helm/ocaml/cic/libraryObjects.mli
@@ -34,3 +34,8 @@ val eq_ind_URI : eq:UriManager.uri -> UriManager.uri
 val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri
 val trans_eq_URI : eq:UriManager.uri -> UriManager.uri
 val sym_eq_URI : eq:UriManager.uri -> UriManager.uri
+
+
+val false_URI : UriManager.uri
+val true_URI : UriManager.uri
+val absurd_URI : UriManager.uri

diff --git a/helm/ocaml/cic/matitaLibraryObjects.ml b/helm/ocaml/cic/matitaLibraryObjects.ml
index 33129ce4c072fb61bca49349492820c28ae261ee..0a4b4f11e035fc32e8d97e2d27a8b8d52a0dfb11 100644 (file)
--- a/helm/ocaml/cic/matitaLibraryObjects.ml
+++ b/helm/ocaml/cic/matitaLibraryObjects.ml
@@ -33,3 +33,10 @@ module Equality =
     let sym_eq_URI = uri "cic:/matita/equality/sym_eq.con"
     let trans_eq_URI = uri "cic:/matita/equality/trans_eq.con"
   end
+
+module Logic =
+  struct
+    let true_URI = uri "cic:/matita/logic/True.ind"
+    let false_URI = uri "cic:/matita/logic/False.ind"
+    let absurd_URI = uri "cic:/matita/logic/absurd.ind"
+  end

diff --git a/helm/ocaml/cic/matitaLibraryObjects.mli b/helm/ocaml/cic/matitaLibraryObjects.mli
index fd254622d293b65a0b267c9afc17b6fa3f27d9a2..57311fde75819cd034dbc315d564480c465c0bdf 100644 (file)
--- a/helm/ocaml/cic/matitaLibraryObjects.mli
+++ b/helm/ocaml/cic/matitaLibraryObjects.mli
@@ -31,3 +31,10 @@ module Equality :
     val sym_eq_URI :    UriManager.uri
     val trans_eq_URI :  UriManager.uri
   end
+
+module Logic :
+  sig
+    val true_URI : UriManager.uri
+    val false_URI : UriManager.uri
+    val absurd_URI : UriManager.uri
+  end

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index cf0db10e65ddead62fd95c9476d504049cd173cc..21fc2b33c1f60aa1d1ded2a76fa812a4992ea97e 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -39,7 +39,7 @@ let rec injection_tac ~term =
     ProofEngineTypes.apply_tactic
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> (
+             when LibraryObjects.is_eq_URI equri -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
@@ -95,7 +95,7 @@ and injection1_tac ~term ~i =
      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      match termty with (* an equality *)
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> (
+             when LibraryObjects.is_eq_URI equri -> (
            match tty with (* some inductive type *)
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -217,7 +217,7 @@ let discriminate'_tac ~term =
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
       match termty with
          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
-          when (U.eq equri HelmLibraryObjects.Logic.eq_URI) -> (
+          when LibraryObjects.is_eq_URI equri -> (
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
@@ -276,8 +276,8 @@ let discriminate'_tac ~term =
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd(HelmLibraryObjects.Logic.false_URI,0,[]))
-                                     else (C.MutInd(HelmLibraryObjects.Logic.true_URI,0,[]))
+                                     then (C.MutInd(LibraryObjects.false_URI,0,[]))
+                                     else (C.MutInd(LibraryObjects.true_URI,0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -287,7 +287,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
                     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(HelmLibraryObjects.Logic.false_URI,0,[])))
+                       ~term:(C.MutInd(LibraryObjects.false_URI,0,[])))
                       status 
                     in
                      (match goals' with

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index c8c9785dae9cdfe094c7c7fed6d543fbb9b3aed6..b86cf43d6048f8efa55cfa00ebabd81e61a006c4 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -37,7 +37,7 @@ let absurd_tac ~term =
     then ProofEngineTypes.apply_tactic 
       (P.apply_tac 
          ~term:(
-           C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; 
+           C.Appl [(C.Const (LibraryObjects.absurd_URI , [] )) ; 
                   term ; ty])
       ) 
       status
@@ -61,7 +61,7 @@ let contradiction_tac =
            ~start:
              (EliminationTactics.elim_type_tac 
                 ~term:
-                  (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
+                  (C.MutInd (LibraryObjects.false_URI, 0, [])))
            ~continuation: VariousTactics.assumption_tac))
     status
    with