some makefile work

[helm.git] / helm / ocaml / tactics / paramodulation / saturation.ml

diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml
index 07fbaa41c5a2e5b0a6c35557bcbfccbfaa561e7b..9c4dce4603cd055d9db0709beb7d2ad18caaceeb 100644 (file)
--- 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