Bug fixed: metasenv used in place of metasenv' during rewriting in an

[helm.git] / helm / ocaml / acic_content / acic2content.ml

diff --git a/helm/ocaml/acic_content/acic2content.ml b/helm/ocaml/acic_content/acic2content.ml
index 72699f7e3cb2b584da6617a278a1b1f611945abd..57b8502bb3ac4e35029178490e0726766b94f1de 100644 (file)
--- a/helm/ocaml/acic_content/acic2content.ml
+++ b/helm/ocaml/acic_content/acic2content.ml
@@ -32,6 +32,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* $Id$ *)
+
 let object_prefix = "obj:";;
 let declaration_prefix = "decl:";;
 let definition_prefix = "def:";;
@@ -574,7 +576,6 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                K.ArgProof
                 {body with K.proof_name = name; K.proof_context=context} in
           List.map2 build_proof patterns name_and_arities in
-        let teid = get_id te in
         let context,term =
           (match 
              build_subproofs_and_args 
@@ -799,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