From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Jun 2006 14:39:14 +0000 (+0000)
Subject: 1. the default for the default equality/absurd/true/false URIs used to be
X-Git-Tag: 0.4.95@7852~1352
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec7717f5e0dd4c295ba1cfd57a0a6a46170490ef;p=helm.git

1. the default for the default equality/absurd/true/false URIs used to be
   the Coq ones; now it is None
2. legacy/coq.ma changed to set the default URIs for Coq
3. generation of inversion principles is now branched again
---

diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml
index 223b24edd..df653eb9a 100644
--- a/components/cic/libraryObjects.ml
+++ b/components/cic/libraryObjects.ml
@@ -27,28 +27,17 @@
 
 (**** TABLES ****)
 
-let default_eq_URIs =
- [HelmLibraryObjects.Logic.eq_URI,
-      HelmLibraryObjects.Logic.sym_eq_URI,
-      HelmLibraryObjects.Logic.trans_eq_URI,
-      HelmLibraryObjects.Logic.eq_ind_URI,
-      HelmLibraryObjects.Logic.eq_ind_r_URI];;
-
-let default_true_URIs = [HelmLibraryObjects.Logic.true_URI]
-let default_false_URIs = [HelmLibraryObjects.Logic.false_URI]
-let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI]
+let default_eq_URIs = []
+let default_true_URIs = []
+let default_false_URIs = []
+let default_absurd_URIs = []
 
 (* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
-let eq_URIs_ref =
- ref [HelmLibraryObjects.Logic.eq_URI,
-      HelmLibraryObjects.Logic.sym_eq_URI,
-      HelmLibraryObjects.Logic.trans_eq_URI,
-      HelmLibraryObjects.Logic.eq_ind_URI,
-      HelmLibraryObjects.Logic.eq_ind_r_URI];;
+let eq_URIs_ref = ref default_eq_URIs;;
 
-let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI]
-let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI]
-let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI]
+let true_URIs_ref = ref default_true_URIs
+let false_URIs_ref = ref default_false_URIs
+let absurd_URIs_ref = ref default_absurd_URIs
 
 
 (**** SET_DEFAULT ****)
@@ -86,7 +75,9 @@ let reset_defaults () =
 
 (**** LOOKUP FUNCTIONS ****)
 
-let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq
+let eq_URI () =
+ try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
+ with Failure "hd" -> None
 
 let is_eq_URI uri =
  List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
@@ -121,6 +112,9 @@ let eq_ind_r_URI ~eq:uri =
   let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
  with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
 
-let true_URI () = List.hd !true_URIs_ref
-let false_URI () = List.hd !false_URIs_ref
-let absurd_URI () = List.hd !absurd_URIs_ref
+let true_URI () =
+ try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
+let false_URI () =
+ try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
+let absurd_URI () =
+ try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli
index 1fa0dcc83..7c31bf2bf 100644
--- a/components/cic/libraryObjects.mli
+++ b/components/cic/libraryObjects.mli
@@ -26,7 +26,7 @@
 val set_default : string -> UriManager.uri list -> unit
 val reset_defaults : unit -> unit 
 
-val eq_URI : unit -> UriManager.uri
+val eq_URI : unit -> UriManager.uri option
 
 val is_eq_URI : UriManager.uri -> bool
 val is_eq_ind_URI : UriManager.uri -> bool
@@ -42,7 +42,7 @@ val trans_eq_URI : eq:UriManager.uri -> UriManager.uri
 val sym_eq_URI : eq:UriManager.uri -> UriManager.uri
 
 
-val false_URI : unit -> UriManager.uri
-val true_URI : unit -> UriManager.uri
-val absurd_URI : unit -> UriManager.uri
+val false_URI : unit -> UriManager.uri option
+val true_URI : unit -> UriManager.uri option
+val absurd_URI : unit -> UriManager.uri option
 
diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a09baafe1..413cc986c 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -336,7 +336,7 @@ let add_obj refinement_toolkit uri obj =
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @ 
           generate_elimination_principles uri refinement_toolkit;
-	      (* uris := !uris @ generate_inversion refinement_toolkit uri obj; *)
+	uris := !uris @ generate_inversion refinement_toolkit uri obj;
         let rec get_record_attrs =
           function
           | [] -> None
diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 0ffa2c52b..4c7f5148d 100644
--- 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
diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml
index cca2c1a59..b1727fb7d 100644
--- a/components/tactics/equalityTactics.ml
+++ b/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]))
diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index f5e2a8476..74117f710 100644
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -171,6 +171,7 @@ let isSetType paramty = ((Pervasives.compare
   (get_sort_type paramty)
   (Cic.Sort Cic.Prop)) != 0) 
 
+exception EqualityNotDefinedYet
 let private_inversion_tac ~term =
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -181,7 +182,11 @@ let private_inversion_tac ~term =
  
  (*DEBUG*) debug_print (lazy  ("private inversion begins"));
  let (_,metasenv,_,_) = proof in
- let uri_of_eq = LibraryObjects.eq_URI () in
+ let uri_of_eq =
+  match LibraryObjects.eq_URI () with
+     None -> raise EqualityNotDefinedYet
+  | Some uri -> uri
+ in
  let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
  let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
  let uri = baseuri_of_term termty in  
diff --git a/components/tactics/inversion.mli b/components/tactics/inversion.mli
index 1471f5dbc..2c8b996ff 100644
--- a/components/tactics/inversion.mli
+++ b/components/tactics/inversion.mli
@@ -24,5 +24,6 @@
  *)
 
 val isSetType: Cic.term -> bool
+exception EqualityNotDefinedYet (* raised by private_inversion_tac only *)
 val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic
 val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic
diff --git a/components/tactics/inversion_principle.ml b/components/tactics/inversion_principle.ml
index b16b133ba..8031e7bbd 100644
--- a/components/tactics/inversion_principle.ml
+++ b/components/tactics/inversion_principle.ml
@@ -145,7 +145,7 @@ let build_inversion uri obj =
  if List.length (list_of_prod arity) = (nleft + 1) then
   None
  else
-  begin
+  try
    let arity_l = cut_last (list_of_prod arity) in
    let rightparam_tys = cut_first nleft arity_l in
    let theorem = build_theorem rightparam_tys arity_l arity cons_list 
@@ -194,7 +194,8 @@ let build_inversion uri obj =
    Some
     (inversor_uri,
     Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
-  end
+  with
+   Inversion.EqualityNotDefinedYet -> None
 ;;
 
 let init () = ();;
diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index b9c053653..8822c527c 100644
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -205,19 +205,22 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
 (*  match main with *)
 (*      None -> raise Goal_is_not_an_equation *)
 (*    | Some (m,l) -> *)
- let m, l =
+ let l =
    let eq_URI =
-     let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
-     UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+    match LibraryObjects.eq_URI () with
+       None -> None
+     | Some s ->
+        Some
+         (UriManager.uri_of_string
+          (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
    in
-   match main with
-   | None -> eq_URI, []
-   | Some (m, l) when UriManager.eq m eq_URI -> m, l
-   | Some (m, l) -> eq_URI, []
+   match eq_URI,main with
+   | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
+   | _,_ -> []
  in
  Printf.printf "\nSome (m, l): %s, [%s]\n\n"
-   (UriManager.string_of_uri m)
-   (String.concat "; " (List.map UriManager.string_of_uri l));
+   (UriManager.string_of_uri (List.hd l))
+   (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
  let set = signature_of_hypothesis context in
  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
@@ -226,7 +229,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
  let set = close_with_constructors set metasenv context in
  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
- let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let set = List.fold_right Constr.UriManagerSet.remove l set in
  let uris =
    sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
  let uris = List.filter nonvar (List.map snd uris) in
diff --git a/components/tactics/negationTactics.ml b/components/tactics/negationTactics.ml
index 7ee79e534..c973d75f4 100644
--- a/components/tactics/negationTactics.ml
+++ b/components/tactics/negationTactics.ml
@@ -33,13 +33,18 @@ let absurd_tac ~term =
   let module P = PrimitiveTactics in
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
+  let absurd_URI =
+   match LibraryObjects.absurd_URI () with
+      Some uri -> uri
+    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command"))
+  in
   let ty_term,_ = 
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
     if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
     then ProofEngineTypes.apply_tactic 
       (P.apply_tac 
          ~term:(
-           C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ; 
+           C.Appl [(C.Const (absurd_URI, [] )) ; 
 	           term ; ty])
       ) 
       status
@@ -55,6 +60,11 @@ let contradiction_tac =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals 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
    try
     ProofEngineTypes.apply_tactic (
      T.then_
@@ -62,8 +72,7 @@ let contradiction_tac =
       ~continuation:(
 	 T.then_
            ~start:
-             (EliminationTactics.elim_type_tac 
-                (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+             (EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
            ~continuation: VariousTactics.assumption_tac))
     status
    with 
diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 3979c0529..3bff5b574 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -737,7 +737,7 @@ let build_goal_proof l initial ty se =
 let refl_proof ty term = 
   Cic.Appl 
     [Cic.MutConstruct 
-       (LibraryObjects.eq_URI (), 0, 1, []);
+       (Utils.eq_URI (), 0, 1, []);
        ty; term]
 ;;
 
@@ -912,14 +912,14 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = LibraryObjects.eq_URI () in
+  let eq_uri = Utils.eq_URI () in
   let iseq uri = UriManager.eq uri eq_uri in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
@@ -951,7 +951,7 @@ let term_of_equality equality =
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
   in
   snd (
     List.fold_right
diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 9c5ea281b..e72ed64da 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -583,7 +583,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
       let name = C.Name "x" in
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
-          C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+          C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
                   S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
@@ -900,7 +900,7 @@ let superposition_right
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+        C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
                 S.lift 1 eq_ty; l; r]
       in
       bo',
diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 6a21bb173..91fcee8a2 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -211,7 +211,7 @@ let find_equalities context proof =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let eq_uri = LibraryObjects.eq_URI () in
+  let eq_uri = Utils.eq_URI () in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -349,7 +349,7 @@ let find_library_equalities dbd context status maxmeta =
        eqs)
   in
   let eq_uri1 = eq_XURI ()
-  and eq_uri2 = LibraryObjects.eq_URI () in
+  and eq_uri2 = Utils.eq_URI () in
   let iseq uri =
     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
   in
diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index a26ec0f73..1282ed27f 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -889,7 +889,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 *)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
-    when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+    when UriManager.eq uri (Utils.eq_URI ()) ->
       (let goal_equation = 
          Equality.mk_equality
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
@@ -946,7 +946,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
 (*     in *)
     let ok, proof =
       (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
-      let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+      let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
       match fst goals with
         | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ 
             when left = right && iseq uri -> 
@@ -1195,7 +1195,7 @@ let given_clause_fullred dbd env goals theorems passive active =
     (given_clause_fullred dbd env goals theorems passive) active
 *)
 
-let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());;
+let iseq uri = UriManager.eq uri (Utils.eq_URI ());;
 
 let check_if_goal_is_identity env = function
   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
@@ -1671,7 +1671,7 @@ let saturate
         context_hyp @ thms, []
       else
         let refl_equal =
-          let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+          let us = UriManager.string_of_uri (Utils.eq_URI ()) in
           UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
         in
         let t = CicUtil.term_of_uri refl_equal in
diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 072d64f66..c2b1905f8 100644
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -724,14 +724,18 @@ let string_of_pos = function
   | Right -> "Right"
 ;;
 
-
-let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
-let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
-let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_URI () =
+ match LibraryObjects.eq_URI () with
+    None -> assert false
+  | Some uri -> uri
+
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(eq_URI ())
 let eq_XURI () =
-  let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+  let s = UriManager.string_of_uri (eq_URI ()) in
   UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(eq_URI ())
 
 let metas_of_term t = 
   List.map fst (CicUtil.metas_of_term t)
diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli
index f44cab460..2f1533e69 100644
--- a/components/tactics/paramodulation/utils.mli
+++ b/components/tactics/paramodulation/utils.mli
@@ -87,6 +87,7 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int
 
 val debug_print: string Lazy.t -> unit
 
+val eq_URI: unit -> UriManager.uri
 val eq_ind_URI: unit -> UriManager.uri
 val eq_ind_r_URI: unit -> UriManager.uri
 val sym_eq_URI: unit -> UriManager.uri
diff --git a/matita/library/legacy/coq.ma b/matita/library/legacy/coq.ma
index 76da7d898..e7a5615d9 100644
--- a/matita/library/legacy/coq.ma
+++ b/matita/library/legacy/coq.ma
@@ -14,6 +14,20 @@
 
 set "baseuri" "cic:/matita/legacy/coq/".
 
+default "equality"
+ cic:/Coq/Init/Logic/eq.ind
+ cic:/Coq/Init/Logic/sym_eq.con
+ cic:/Coq/Init/Logic/trans_eq.con
+ cic:/Coq/Init/Logic/eq_ind.con
+ cic:/Coq/Init/Logic/eq_ind_r.con. 
+
+default "true"
+ cic:/Coq/Init/Logic/True.ind. 
+default "false"
+ cic:/Coq/Init/Logic/False.ind. 
+default "absurd"
+ cic:/Coq/Init/Logic/absurd.con. 
+
 (* aritmetic operators *)
 
 interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).