]> matita.cs.unibo.it Git - helm.git/commitdiff
Fix_proof should recursively work on explicit substs.
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 27 Nov 2006 13:46:19 +0000 (13:46 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 27 Nov 2006 13:46:19 +0000 (13:46 +0000)
For the moment this is done for constants.

components/tactics/paramodulation/saturation.ml

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