From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 27 Nov 2006 13:46:19 +0000 (+0000)
Subject: Fix_proof should recursively work on explicit substs.
X-Git-Tag: 0.4.95@7852~772
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a996266824ef41b59130440804ef1777137802e7;p=helm.git

Fix_proof should recursively work on explicit substs.
For the moment this is done for constants.
---

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