X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=b2348f732a0b014fa26d515e28b8b9cb0401bd57;hb=06a089726af079d5b2fe42ba78632565dad0eb3e;hp=7ef8d41acdf6f43be4a409a3d66f586e4057df08;hpb=62e3a3ce3ac21ab25074ad2af1883a4b0cbc62be;p=helm.git

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