hSqlite3.ml used create_fun_2 to define REGEXP.

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

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80..e453d95c12c968a3cd696b157db950a6f87408e7 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -621,6 +621,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
+    let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
       let bo = 
@@ -858,6 +859,7 @@ let superposition_right bag
       Equality.open_equality  equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
 
+    let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
     let newgoal, newproof =
       (* qua *)
       let bo' =
@@ -1003,10 +1005,8 @@ 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
-    (* patch?? 
-    let bo' = t in
-    let ty = apply_subst subst ty in *)
+    let bo' = apply_subst subst 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)