From a996266824ef41b59130440804ef1777137802e7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 27 Nov 2006 13:46:19 +0000 Subject: [PATCH] Fix_proof should recursively work on explicit substs. For the moment this is done for constants. --- components/tactics/paramodulation/saturation.ml | 9 +++++++++ 1 file changed, 9 insertions(+) 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 -- 2.39.2