X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Fsaturation.ml;fp=helm%2Focaml%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=9c4dce4603cd055d9db0709beb7d2ad18caaceeb;hb=c051f623926cdc3b744c38ba393c0a9c7622d299;hp=07fbaa41c5a2e5b0a6c35557bcbfccbfaa561e7b;hpb=0ef468f9000a8e9c391cc8ade2f9aea35e878305;p=helm.git

diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml
index 07fbaa41c..9c4dce460 100644
--- a/helm/ocaml/tactics/paramodulation/saturation.ml
+++ b/helm/ocaml/tactics/paramodulation/saturation.ml
@@ -483,6 +483,22 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   
   let demodulate table current = 
     let newmeta, newcurrent =
+      let _ =
+        let w, proof, (eq_ty, left, right, order), metas, args = current in
+	let metasenv, context, ugraph = env in
+	let metasenv' = metasenv @ metas in
+	try
+	  CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+	  CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+	with 
+	    CicUtil.Meta_not_found _ as exn ->
+	      begin
+		prerr_endline "siamo in forward_simplify"; 
+		prerr_endline (CicPp.ppterm left);
+		prerr_endline (CicPp.ppterm right);
+		raise exn
+	      end 
+      in
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
@@ -568,6 +584,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   
   let demodulate sign table target =
     let newmeta, newtarget =
+      let _ =
+        let w, proof, (eq_ty, left, right, order), metas, args = target in
+	let metasenv, context, ugraph = env in
+	let metasenv' = metasenv @ metas in
+	try
+	  CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+	  CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+	with 
+	    CicUtil.Meta_not_found _ as exn ->
+	      begin
+		prerr_endline "siamo in forward_simplify_new"; 
+		prerr_endline (CicPp.ppterm left);
+		prerr_endline (CicPp.ppterm right);
+		raise exn
+	      end 
+      in
       Indexing.demodulation_equality !maxmeta env table sign target in
     maxmeta := newmeta;
     newtarget