X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=a52109e46ad475e526eb9d46d63c74945d5f80a9;hb=04dc7b17e463fa9c75ac91e1df88bf37ed009914;hp=6e792201964824db331fce7d3fc7813bac10be2a;hpb=b109559ac6795075508fd5c231a1bf2a3223031a;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 6e7922019..a52109e46 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -711,7 +711,7 @@ let activate_theorem (active, passive) =
 ;;
 
 
-
+(*
 let simplify_theorems bag env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
@@ -741,7 +741,7 @@ let simplify_theorems bag env theorems ?passive (active_list, active_table) =
       let p_theorems = List.map (mapfun passive_table) p_theorems in
       List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
 ;;
-
+*)
 
 let rec simpl bag eq_uri env e others others_simpl =
   let active = others @ others_simpl in
@@ -1277,10 +1277,11 @@ let fix_proof metasenv context all_implicits p =
 	  let metasenv,s = aux metasenv n s in
 	  let metasenv,t = aux metasenv (n+1) t in
 	    metasenv,Cic.Prod(name,s,t)
-      | Cic.LetIn(name,s,t) ->
+      | Cic.LetIn(name,s,ty,t) ->
 	  let metasenv,s = aux metasenv n s in
+	  let metasenv,ty = aux metasenv n ty in
 	  let metasenv,t = aux metasenv (n+1) t in
-	    metasenv,Cic.LetIn(name,s,t)	      
+	    metasenv,Cic.LetIn(name,s,ty,t)
       | Cic.Const(uri,ens) -> 
 	  let metasenv,ens =
 	    List.fold_right 
@@ -1361,20 +1362,33 @@ let build_proof
     prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
     raise exn
   in
+  let old_insert_coercions = !CicRefine.insert_coercions in
   let goal_proof,goal_ty,real_menv,_ = 
     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
     try
             debug_print (lazy (CicPp.ppterm goal_proof));
-      CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+            CicRefine.insert_coercions := false;
+            let res = 
+              CicRefine.type_of_aux' 
+                real_menv context goal_proof CicUniv.empty_ugraph
+            in
+            CicRefine.insert_coercions := old_insert_coercions;
+            res
     with 
       | CicRefine.RefineFailure s 
       | CicRefine.Uncertain s 
       | CicRefine.AssertFailure s as exn -> 
+          CicRefine.insert_coercions := old_insert_coercions;
           pp_error goal_proof names (Lazy.force s) exn
       | CicUtil.Meta_not_found i as exn ->
+          CicRefine.insert_coercions := old_insert_coercions;
           pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
       | Invalid_argument "list_fold_left2" as exn ->
+          CicRefine.insert_coercions := old_insert_coercions;
           pp_error goal_proof names "Invalid_argument: list_fold_left2" exn 
+      | exn ->
+          CicRefine.insert_coercions := old_insert_coercions;
+          raise exn
   in     
   let subst_side_effects,real_menv,_ = 
     try