X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=b2348f732a0b014fa26d515e28b8b9cb0401bd57;hb=5682bf51adcde903c53a96e05475a7ded8fb255d;hp=d9472601c958c96b62526c9af50c11e1ac5a6f9b;hpb=06b128f1107fd579a696b83b2f8255f83ab29a92;p=helm.git

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d9472601c..b2348f732 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/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