X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=b2348f732a0b014fa26d515e28b8b9cb0401bd57;hb=0de62d69d01f334e0300633d22b63c91edd8fc7f;hp=d9472601c958c96b62526c9af50c11e1ac5a6f9b;hpb=cee1c02ad6a113b711b9d93176296cf16b9ec351;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index d9472601c..b2348f732 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1280,6 +1280,15 @@ 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.LetIn(name,s,t)	      
+      | Cic.Const(uri,ens) -> 
+	  let metasenv,ens =
+	    List.fold_right 
+	      (fun (v,a) (metasenv,ens) -> 
+		 let metasenv,a' = aux metasenv n a in
+		   metasenv,(v,a')::ens)
+	      ens (metasenv,[])
+	  in
+	  metasenv,Cic.Const(uri,ens)
       | t -> metasenv,t
   in
   aux metasenv 0 p 
@@ -1531,7 +1540,6 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
   match LibraryObjects.eq_URI () with
     | None -> active, passive, !maxmeta
     | Some eq_uri -> 
@@ -1593,7 +1601,6 @@ let given_clause
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in