Rewriting steps using the rewriting principles in the library of Matita are

now supported.

diff --git a/helm/ocaml/acic_content/acic2content.ml b/helm/ocaml/acic_content/acic2content.ml
index ed4eafb4efd2a39774f331cc1b3d6b78ab31da0d..57b8502bb3ac4e35029178490e0726766b94f1de 100644 (file)
--- a/helm/ocaml/acic_content/acic2content.ml
+++ b/helm/ocaml/acic_content/acic2content.ml
@@ -800,7 +800,9 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
   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 

diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml
index cc04322fa970d94606e237dd034f5f07aab7fab1..adbc219cc3fd72771b314a3e61eeea85a98cfc52 100644 (file)
--- a/helm/ocaml/cic/libraryObjects.ml
+++ b/helm/ocaml/cic/libraryObjects.ml
@@ -91,6 +91,12 @@ let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq
 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

diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli
index f87065980adec57ed2dc253e7ce5d0cf92045aa7..eca5a0d902c309f3e386c91e4f1f3e96ce76ff61 100644 (file)
--- a/helm/ocaml/cic/libraryObjects.mli
+++ b/helm/ocaml/cic/libraryObjects.mli
@@ -29,6 +29,8 @@ val reset_defaults : unit -> unit
 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;;