X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=a4bdef1a2a48b0121246ead95c73f21edb56183a;hb=ff074375003b7b0e3d38e2742ff1d6098a0dab57;hp=7b545dd47c5b72a1cec282bc92f40c25b57c60b7;hpb=d8d939cc3f78a805a3c16f715912ecd96c302592;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 7b545dd47..a4bdef1a2 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -534,7 +534,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -582,90 +582,10 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
-      if sign = Utils.Positive then
           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
           (Cic.Lambda (name, ty, bo'))))))
-      else
-        assert false
-(*
-        begin
-        prerr_endline "***************************************negative";
-        let metaproof = 
-          incr maxmeta;
-          let irl =
-            CicMkImplicit.identity_relocation_list_for_metavariable context in
-(*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(*        print_newline (); *)
-          C.Meta (!maxmeta, irl)
-        in
-          let eq_found =
-            let proof'_old' =
-              let termlist =
-                if pos = Utils.Left then [ty; what; other]
-                else [ty; other; what]
-              in
-              Equality.ProofSymBlock (termlist, proof'_old)
-            in
-            let proof'_new' = assert false (* not implemented *) in
-            let what, other =
-              if pos = Utils.Left then what, other else other, what
-            in
-            pos, 
-              Equality.mk_equality 
-                (0, (proof'_new',proof'_old'), 
-                (ty, other, what, Utils.Incomparable),menv')
-          in
-          let target_proof =
-            let pb =
-              Equality.ProofBlock 
-                (subst, eq_URI, (name, ty), bo',
-                 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
-            in
-            assert false, (* not implemented *)
-            (match snd proof with
-            | Equality.BasicProof _ ->
-                (* print_endline "replacing a BasicProof"; *)
-                pb
-            | Equality.ProofGoalBlock (_, parent_proof) ->
-  (* print_endline "replacing another ProofGoalBlock"; *)
-                Equality.ProofGoalBlock (pb, parent_proof)
-            | _ -> assert false)
-          in
-        let refl =
-          C.Appl [C.MutConstruct (* reflexivity *)
-                    (LibraryObjects.eq_URI (), 0, 1, []);
-                  eq_ty; if is_left then right else left]          
-        in
-        (bo,
-         (assert false, (* not implemented *)
-         Equality.ProofGoalBlock 
-           (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
-      end
-*)
     in
-    let newmenv = (* Inference.filter subst *) menv in
-(*
-    let _ = 
-      if Utils.debug_metas then 
-        try ignore(CicTypeChecker.type_of_aux'
-          newmenv context 
-            (Equality.build_proof_term newproof) ugraph);
-          () 
-        with exc ->                   
-          prerr_endline "sempre lui";
-          prerr_endline (Subst.ppsubst subst);
-          prerr_endline (CicPp.ppterm 
-            (Equality.build_proof_term newproof));
-          prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
-          prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
-          prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
-          prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
-          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
-            newmenv));
-          raise exc;
-      else () 
-    in
-*)
+    let newmenv = menv in
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
     let stat = (eq_ty, left, right, ordering) in
@@ -689,7 +609,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality ?from eq_uri newmeta env table sign newtarget
+            demodulation_equality ?from eq_uri newmeta env table newtarget
     | None ->
         let res = demodulation_aux metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
@@ -700,7 +620,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality ?from eq_uri newmeta env table sign newtarget
+                   demodulation_equality ?from eq_uri newmeta env table newtarget
           | None ->
               newmeta, target
   in