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 7ef8d41acdf6f43be4a409a3d66f586e4057df08..b2348f732a0b014fa26d515e28b8b9cb0401bd57 100644 (file)
--- 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