Modifications to auto due to the introduction of the universe in

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 7bbc4d43ca7fb7548a6397f08ffc16f473d9c648..28c22a64e34b8fd7ccf99d34ba4903f7f526aa0f 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -1003,8 +1003,11 @@ let build_newgoal bag context goal posu rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = (*apply_subst subst*) t in 
-    let name = Cic.Name "x" in
+    let bo' = (*apply_subst subst*) t in
+    (* patch?? 
+    let bo' = t in
+    let ty = apply_subst subst ty in *)
+    let name = Cic.Name "x" in 
     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)
   in