Fix_proof should recursively work on explicit substs.

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index d9472601c958c96b62526c9af50c11e1ac5a6f9b..b2348f732a0b014fa26d515e28b8b9cb0401bd57 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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 
@@ -1531,7 +1540,6 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
   match LibraryObjects.eq_URI () with
     | None -> active, passive, !maxmeta
     | Some eq_uri -> 
@@ -1593,7 +1601,6 @@ let given_clause
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in