match li with
C.AConst (sid,uri,exp_named_subst)::args ->
if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or
- UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI then
+ UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI or
+ LibraryObjects.is_eq_ind_URI uri or
+ LibraryObjects.is_eq_ind_r_URI uri then
let subproofs,arg =
(match
build_subproofs_and_args
let is_eq_URI uri =
List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
+let is_eq_ind_URI uri =
+ 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
+
let sym_eq_URI ~eq:uri =
try
let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
val eq_URI : unit -> UriManager.uri
val is_eq_URI : UriManager.uri -> bool
+val is_eq_ind_URI : UriManager.uri -> bool
+val is_eq_ind_r_URI : UriManager.uri -> bool
exception NotRecognized;;