* 'default "equality"' command changed to consider also

[helm.git] / helm / software / components / cic / libraryObjects.ml

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index d8af91a6f01b4dc0dab2d3708306784a67733891..579c21eede3a9f2f2e44023d180377fcf2282341 100644 (file)
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -56,12 +56,14 @@ let insert_unique e extract l =
 let set_default what l =
   match what,l with
   "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;
-              eq_ind_r_URI;eq_f_URI;eq_f_sym_URI] ->
+              eq_ind_r_URI;eq_rec_URI;eq_rec_r_URI;eq_rect_URI;
+              eq_rect_r_URI;eq_f_URI;eq_f_sym_URI] ->
       eq_URIs_ref :=
        insert_unique
          (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,
-          eq_ind_r_URI,eq_f_URI,eq_f_sym_URI)
-        (fun x,_,_,_,_,_,_ -> x) !eq_URIs_ref
+          eq_ind_r_URI,eq_rec_URI,eq_rec_r_URI,eq_rect_URI,
+          eq_rect_r_URI,eq_f_URI,eq_f_sym_URI)
+        (fun x,_,_,_,_,_,_,_,_,_,_ -> x) !eq_URIs_ref
   | "true",[true_URI] ->
       true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
   | "false",[false_URI] ->
@@ -82,11 +84,11 @@ let reset_defaults () =
 
 (**** LOOKUP FUNCTIONS ****)
 let eq_URI () =
- try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
+ 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
+ List.exists (fun (eq,_,_,_,_,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
 
 let is_eq_refl_URI uri =
   let urieq = UriManager.strip_xpointer uri in
@@ -95,22 +97,32 @@ let is_eq_refl_URI uri =
 ;;
 
 let is_eq_ind_URI uri =
- List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
+ List.exists (fun (_,_,_,eq_ind,_,_,_,_,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref
 let is_eq_ind_r_URI uri =
- List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
+ List.exists (fun (_,_,_,_,eq_ind_r,_,_,_,_,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref
+let is_eq_rec_URI uri =
+ List.exists (fun (_,_,_,_,_,eq_rec,_,_,_,_,_) -> UriManager.eq eq_rec uri) !eq_URIs_ref
+let is_eq_rec_r_URI uri =
+ List.exists (fun (_,_,_,_,_,_,eq_rec_r,_,_,_,_) -> UriManager.eq eq_rec_r uri) !eq_URIs_ref
+let is_eq_rect_URI uri =
+ List.exists (fun (_,_,_,_,_,_,_,eq_rect,_,_,_) -> UriManager.eq eq_rect uri) !eq_URIs_ref
+let is_eq_rect_r_URI uri =
+ List.exists (fun (_,_,_,_,_,_,_,_,eq_rect_r,_,_) -> UriManager.eq eq_rect_r uri) !eq_URIs_ref
 let is_trans_eq_URI uri = 
- List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
+ List.exists (fun (_,_,trans_eq,_,_,_,_,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref
 let is_sym_eq_URI uri =
- List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
+ List.exists (fun (_,sym_eq,_,_,_,_,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref
 let is_eq_f_URI uri =
- List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
+ List.exists (fun (_,_,_,_,_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref
 let is_eq_f_sym_URI uri =
- List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
+ List.exists (fun (_,_,_,_,_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref
 
 let in_eq_URIs uri =  
   is_eq_URI uri || is_eq_refl_URI uri || is_eq_ind_URI uri || 
-  is_eq_ind_r_URI uri || is_trans_eq_URI uri || is_sym_eq_URI uri || 
-  is_eq_f_URI uri || is_eq_f_sym_URI uri
+  is_eq_ind_r_URI uri || is_eq_rec_URI uri || is_eq_rec_r_URI uri ||
+  is_eq_rect_URI uri || is_eq_rect_r_URI uri ||
+  is_trans_eq_URI uri || is_sym_eq_URI uri || is_eq_f_URI uri ||
+  is_eq_f_sym_URI uri
 
 
  
@@ -120,39 +132,59 @@ let eq_refl_URI ~eq:uri =
  
 let sym_eq_URI ~eq:uri =
  try
-  let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  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 trans_eq_URI ~eq:uri =
  try
-  let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  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 eq_ind_URI ~eq:uri =
  try
-  let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  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 eq_ind_r_URI ~eq:uri =
  try
-  let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  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 eq_rec_URI ~eq:uri =
+ try
+  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 eq_rec_r_URI ~eq:uri =
+ try
+  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 eq_rect_URI ~eq:uri =
+ try
+  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 eq_rect_r_URI ~eq:uri =
+ try
+  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 eq_f_URI ~eq:uri =
  try
-  let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  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 eq_f_sym_URI ~eq:uri =
  try
-  let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
+  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 eq_URI_of_eq_f_URI eq_f_URI = 
   try
-  let x,_,_,_,_,_,_ = 
-    List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref 
+  let x,_,_,_,_,_,_,_,_,_,_ = 
+    List.find (fun _,_,_,_,_,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref 
   in x
  with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI))