X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=f74cd179766da34f1c8db1701bca4a69eaa3d250;hb=fc7466b8428ea409d97c0dfa347de9f4f51cb582;hp=6582bfd258f09d5e5619345e135b49a26d6daec0;hpb=fd65a0a393bfb43d88ff936f40f045511e900e26;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 6582bfd25..f74cd1797 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -26,9 +26,135 @@
 (* $Id$ *)
 
 open Utils;;
+open Printf;;
 
 let metas_of_proof_time = ref 0.;;
 let metas_of_term_time = ref 0.;;
+(*
+type substitution = Cic.substitution 
+let apply_subst = CicMetaSubst.apply_subst
+let apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
+let ppsubst = CicMetaSubst.ppsubst
+let buildsubst n context t ty = (n,(context,t,ty))
+let flatten_subst subst =
+    List.map
+      (fun (i, (context, term, ty)) ->
+	 let context = (*` apply_subst_context subst*) context in
+	 let term = apply_subst subst term in
+	 let ty = apply_subst subst ty in  
+	 (i, (context, term, ty))) subst
+let rec lookup_subst meta subst =
+  match meta with
+  | Cic.Meta (i, _) -> (
+      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
+      in lookup_subst t subst 
+      with Not_found -> meta
+    )
+  | _ -> meta
+;;
+*)
+
+(* naif version of apply subst; the local context of metas is ignored;
+we assume the substituted term must be lifted according to the nesting
+depth of the meta. Alternatively, ee could used implicit instead of
+metas *)
+
+
+type substitution = (int * Cic.term) list 
+
+let apply_subst subst term =
+ let rec aux k t =
+   match t with
+       Cic.Rel _ -> t
+     | Cic.Var (uri,exp_named_subst) -> 
+	 let exp_named_subst' =
+           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	 in
+	   Cic.Var (uri, exp_named_subst')
+    | Cic.Meta (i, l) -> 
+        (try
+          aux k (CicSubstitution.lift k (List.assoc i subst)) 
+         with Not_found -> t)
+    | Cic.Sort _
+    | Cic.Implicit _ -> t
+    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
+    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
+    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
+    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+    | Cic.Appl [] -> assert false
+    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
+    | Cic.Const (uri,exp_named_subst) ->
+	let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	in
+	  if exp_named_subst' != exp_named_subst then
+	    Cic.Const (uri, exp_named_subst')
+	  else
+	    t (* TODO: provare a mantenere il piu' possibile sharing *)
+    | Cic.MutInd (uri,typeno,exp_named_subst) ->
+	let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	in
+	  Cic.MutInd (uri,typeno,exp_named_subst')
+    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+	let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+	in
+	  Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | Cic.MutCase (sp,i,outty,t,pl) ->
+	let pl' = List.map (aux k) pl in
+	  Cic.MutCase (sp, i, aux k outty, aux k t, pl')
+    | Cic.Fix (i, fl) ->
+	let len = List.length fl in
+	let fl' =
+         List.map 
+	   (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
+	in
+	  Cic.Fix (i, fl')
+    | Cic.CoFix (i, fl) ->
+	let len = List.length fl in
+	let fl' =
+          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
+	in
+	  Cic.CoFix (i, fl')
+in
+  aux 0 term
+;;
+
+(* naif version of apply_subst_metasenv: we do not apply the 
+substitution to the context *)
+
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.mem_assoc i subst))
+      metasenv)
+
+let ppsubst subst =
+  String.concat "\n"
+    (List.map
+      (fun (idx, t) ->
+         sprintf "%d:= %s" idx (CicPp.ppterm t))
+       subst)
+;;
+
+let buildsubst n context t ty = (n,t) ;;
+
+let flatten_subst subst = 
+  List.map (fun (i,t) -> i, apply_subst subst t ) subst
+;;
+
+let rec lookup_subst meta subst =
+  match meta with
+    | Cic.Meta (i, _) ->
+	(try
+	  lookup_subst (List.assoc i subst) subst
+	with
+	    Not_found -> meta)
+    | _ -> meta
+;;
 
 type equality =
     int  *               (* weight *)
@@ -41,9 +167,9 @@ type equality =
 
 and proof =
   | NoProof (* term is the goal missing a proof *)
-  | BasicProof of Cic.term
+  | BasicProof of substitution * Cic.term
   | ProofBlock of
-      Cic.substitution * UriManager.uri *
+      substitution * UriManager.uri *
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof 
   | ProofSymBlock of Cic.term list * proof
@@ -71,13 +197,14 @@ let string_of_equality ?env =
 
 let rec string_of_proof = function
   | NoProof -> "NoProof " 
-  | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+  | BasicProof (s, t) -> "BasicProof " ^ 
+      (CicPp.ppterm (apply_subst s t))
   | SubProof (t, i, p) ->
       Printf.sprintf "SubProof(%s, %s, %s)"
         (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
   | ProofSymBlock _ -> "ProofSymBlock"
   | ProofBlock (subst, _, _, _ ,_,_) -> 
-      "ProofBlock" ^ (CicMetaSubst.ppsubst subst)
+      "ProofBlock" ^ (ppsubst subst)
   | ProofGoalBlock (p1, p2) ->
       Printf.sprintf "ProofGoalBlock(%s, %s)"
         (string_of_proof p1) (string_of_proof p2)
@@ -127,7 +254,7 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
     | NoProof ->
         Printf.fprintf stderr "WARNING: no proof!\n";
         noproof
-    | BasicProof term -> term
+    | BasicProof (s,term) -> apply_subst s term
     | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
         do_build_goal_proof proofbit proof
@@ -146,7 +273,7 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        CicMetaSubst.apply_subst subst
+        apply_subst subst
           (Cic.Appl [Cic.Const (eq_URI, []); ty;
                      what; t'; eqproof; other; proof'])
     | SubProof (term, meta_index, proof) ->
@@ -176,10 +303,9 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
         SubProof (term, meta_index, replace_proof newproof p)
     | p -> p
   in
-  do_build_proof proof
+  do_build_proof proof 
 ;;
 
-
 let rec metas_of_term = function
   | Cic.Meta (i, c) -> [i]
   | Cic.Var (_, ens) 
@@ -217,6 +343,7 @@ let rec metas_of_proof p =
     metas_of_term (build_proof_term p)
 ;;
 
+
 exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
@@ -365,17 +492,6 @@ let rec is_simple_term = function
   | _ -> false
 ;;
 
-
-let rec lookup_subst meta subst =
-  match meta with
-  | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
-      in lookup_subst t subst 
-      with Not_found -> meta
-    )
-  | _ -> meta
-;;
-
 let locked menv i =
   List.exists (fun (j,_,_) -> i = j) menv
 ;;
@@ -419,7 +535,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
           assert (not (List.mem_assoc i subst));
-	  let subst = (i, (context, t, ty))::subst in
+	  let subst = (buildsubst i context t ty)::subst in
           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
@@ -450,7 +566,10 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   List.rev subst, menv, ugraph
 ;;
 
-let profiler = HExtlib.profile "flatten"
+let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
+let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
+let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
+let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   let metasenv = metasenv1 @ metasenv2 in
@@ -471,16 +590,16 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
   in
   if Utils.debug_res then
 	    ignore(check_disjoint_invariant subst menv "unif");
-  let flatten subst = 
+  (* let flatten subst = 
     List.map
       (fun (i, (context, term, ty)) ->
-	 let context = CicMetaSubst.apply_subst_context subst context in
-	 let term = CicMetaSubst.apply_subst subst term in
-	 let ty = CicMetaSubst.apply_subst subst ty in  
+	 let context = apply_subst_context subst context in
+	 let term = apply_subst subst term in
+	 let ty = apply_subst subst ty in  
 	   (i, (context, term, ty))) subst 
   in
   let flatten subst = profiler.HExtlib.profile flatten subst in
-  let subst = flatten subst in
+  let subst = flatten subst in *)
     subst, menv, ug
 ;;
 
@@ -497,231 +616,10 @@ let matching1 metasenv1 metasenv2 context t1 t2 ugraph =
 let unification = unification_aux true 
 ;;
 
-
-
-(*
-let unification metasenv1 metasenv2 context t1 t2 ugraph = 
-  let (subst, metasenv, ugraph) = 
-    CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
-  if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "fo_unif");
-  (subst, metasenv, ugraph)
-    
-;;
-*)
-
-
-(*
-let matching_simple metasenv context t1 t2 ugraph =
-  let module C = Cic in
-  let module M = CicMetaSubst in
-  let module U = CicUnification in
-  let lookup meta subst =
-    match meta with
-    | C.Meta (i, _) -> (
-        try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
-        with Not_found -> meta
-      )
-    | _ -> assert false
-  in
-  let rec do_match subst menv s t =
-    match s, t with
-    | s, t when s = t -> subst, menv
-    | s, C.Meta (i, l) ->
-        let filter_menv i menv =
-          List.filter (fun (m, _, _) -> i <> m) menv
-        in
-        let subst, menv =
-          let value = lookup t subst in
-          match value with
-          | value when value = t ->
-              let _, _, ty = CicUtil.lookup_meta i menv in
-              (i, (context, s, ty))::subst, filter_menv i menv
-          | value when value <> s ->
-              raise MatchingFailure
-          | value -> do_match subst menv s value
-        in
-        subst, menv
-    | C.Appl ls, C.Appl lt -> (
-        try
-          List.fold_left2
-            (fun (subst, menv) s t -> do_match subst menv s t)
-            (subst, menv) ls lt
-        with Invalid_argument _ ->
-          raise MatchingFailure
-      )
-    | _, _ ->
-        raise MatchingFailure
-  in
-  let subst, menv = do_match [] metasenv t1 t2 in
-  subst, menv, ugraph
-;;
-*)
-
-(*
-let matching metasenv context t1 t2 ugraph =
-    try
-      let subst, metasenv, ugraph =
-	try
-          unification metasenv context t1 t2 ugraph
-	with CicUtil.Meta_not_found _ as exn ->
-	  Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
-	    (CicPp.ppterm t1) (CicPp.ppterm t2) 
-	    (CicMetaSubst.ppmetasenv [] metasenv);
-	  raise exn
-      in
-      if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-2");
-      let t' = CicMetaSubst.apply_subst subst t1 in
-      if not (meta_convertibility t1 t') then
-        raise MatchingFailure
-      else
-        if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-1");
-        let metas = metas_of_term t1 in
-        let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-          if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua0");
-	  
-	  let subst, metasenv =
-	  List.fold_left
-	    (fun 
-	       (subst,metasenv) s ->
-		 match s with
-		   | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-		       let metasenv' =
-			 List.filter (fun (x, _, _) -> x<>j) metasenv 
-		       in
-			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
-			  (i,c,ty)::metasenv')
-		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in
-	if Utils.debug_res then
-	  ignore(check_disjoint_invariant subst metasenv "qua1");
-(*
-        let fix_subst = function
-          | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-              (j, (c, Cic.Meta (i, lc), ty))
-          | s -> s
-        in
-        let subst = List.map fix_subst subst in *)
-	if CicMetaSubst.apply_subst subst t1 = t1 then
-          subst, metasenv, ugraph
-	else
-	  (prerr_endline "mah"; raise MatchingFailure)
-    with
-    | CicUnification.UnificationFailure _
-    | CicUnification.Uncertain _ ->
-      raise MatchingFailure
-;;
-*)
-
 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 it perform unification in the union metasenv, then check that
 the first metasenv has not changed *)
 
-
-let matching2 metasenv1 metasenv2 context t1 t2 ugraph =
-      let subst, metasenv, ugraph =
-	try
-          unification metasenv1 metasenv2 context t1 t2 ugraph
-	with 
-	    CicUtil.Meta_not_found _ as exn ->
-	      Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
-		(CicPp.ppterm t1) (CicPp.ppterm t2) 
-		(CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2));
-	      raise exn
-	  | CicUnification.UnificationFailure _
-	  | CicUnification.Uncertain _ ->
-	      raise MatchingFailure    
-      in
-      if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-2");
-      (* let us unfold subst *)
-      if metasenv = metasenv1 then 
-	let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-	  subst, metasenv, ugraph (* everything is fine *)
-      else
-	(* let us unfold subst *)
-	(* 
-	let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-        *)
-	  (* let us revert Meta-Meta in subst privileging metasenv1 *)
-	let subst, metasenv =
-	  List.fold_left
-	    (fun 
-	       (subst,metasenv) s ->
-		 match s with
-		   | (i, (c, Cic.Meta (j, lc), ty)) 
-		       when (List.exists (fun (x, _, _)  -> x=i) metasenv1) &&
-			 not (List.exists (fun (x, _)  -> x=j) subst) ->
-		       let metasenv' =
-			 List.filter (fun (x, _, _) -> x<>j) metasenv 
-		       in
-			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
-			  (i,c,ty)::metasenv')
-		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in	
-	(* finally, let us chek again that metasenv = metasenv1 *)
-	if metasenv = metasenv1 then 
-	  subst, metasenv, ugraph
-	else raise MatchingFailure  
-;;
-
-(* debug 
-let matching metasenv1 metasenv2 context t1 t2 ugraph =
-  let rc1 = 
-    try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph)
-    with MatchingFailure -> None
-  in
-  let rc2 = 
-    try 
-      Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph)
-    with MatchingFailure -> None
-  in
-  match rc1,rc2 with
-  | Some (s,m,g) , None -> 
-      prerr_endline (CicPp.ppterm t1);
-      prerr_endline (CicPp.ppterm t2);
-      prerr_endline "SOLO NOI";
-      prerr_endline (CicMetaSubst.ppsubst s);
-      s,m,g
-  | None , Some _ -> 
-      prerr_endline (CicPp.ppterm t1);
-      prerr_endline (CicPp.ppterm t2);
-      prerr_endline "SOLO LUI";
-      assert false
-  | None, None -> raise MatchingFailure 
-  | Some (s,m,g), Some (s',m',g') ->
-      let s = List.sort (fun (i,_) (j,_) -> i - j) s in
-      let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in
-      if s <> s' then 
-	begin
-	  prerr_endline (CicMetaSubst.ppsubst s);
-	  prerr_endline (CicMetaSubst.ppsubst s');
-	  prerr_endline (CicPp.ppterm t1);
-	  prerr_endline (CicPp.ppterm t2);
-	  	end;
-      s,m,g
-*)  
 let matching = matching1;;
 
 let check_eq context msg eq =
@@ -771,7 +669,7 @@ let find_equalities context proof =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof = BasicProof p in
+                    let proof = BasicProof ([],p) in
                     let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -784,7 +682,7 @@ let find_equalities context proof =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof (C.Rel index), stat, []) in
+              let e = (w, BasicProof ([],(C.Rel index)), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -892,7 +790,7 @@ let find_library_equalities dbd context status maxmeta =
     | C.LetIn (_, s, t) | C.Cast (s, t) ->
         (has_vars s) || (has_vars t)
     | _ -> false
-  in
+ in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (uri, term, termty)::tl ->
@@ -921,7 +819,7 @@ let find_library_equalities dbd context status maxmeta =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof = BasicProof p in
+                    let proof = BasicProof ([],p) in
                     let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -931,7 +829,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof term, stat, []) in
+              let e = (w, BasicProof ([],term), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1018,7 +916,7 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
-
+(*
 let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
   let table = Hashtbl.create (List.length args) in
 
@@ -1084,7 +982,7 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
         (Hashtbl.copy table)
   in
   let rec fix_proof = function
-    | NoProof -> NoProof 
+   | NoProof -> NoProof 
     | BasicProof term -> BasicProof (repl term)
     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
         let subst' =
@@ -1111,26 +1009,22 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
   (newmeta +1, neweq)
 ;;
-
+*)
 
 let relocate newmeta menv =
   let subst, metasenv, newmeta = 
     List.fold_right 
-      (fun (i, context, ty) (subst, menv, maxmeta) -> 
-        let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
-        let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
+      (fun (i, context, ty) (subst, menv, maxmeta) ->         
+	let irl = [] (*
+	 CicMkImplicit.identity_relocation_list_for_metavariable context *)
+	in
+        let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in
         let newmeta = maxmeta, context, ty in
         newsubst::subst, newmeta::menv, maxmeta+1) 
       menv ([], [], newmeta+1)
   in
-  let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-  let subst =
-    List.map
-      (fun (i, (context, term, ty)) ->
-	 let context = CicMetaSubst.apply_subst_context subst context in
-	 let term = CicMetaSubst.apply_subst subst term in
-	 let ty = CicMetaSubst.apply_subst subst ty in  
-	 (i, (context, term, ty))) subst in
+  let metasenv = apply_subst_metasenv subst metasenv in
+  let subst = flatten_subst subst in
   subst, metasenv, newmeta
 
 
@@ -1145,20 +1039,29 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
   prerr_endline (string_of_equality eq); *)
   let subst, metasenv, newmeta = relocate newmeta menv in
-  let ty = CicMetaSubst.apply_subst subst ty in
-  let left = CicMetaSubst.apply_subst subst left in
-  let right = CicMetaSubst.apply_subst subst right in
-  let rec fix_proof = function
+(*
+  if newmeta > 2839 then
+    begin
+      prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right);
+      prerr_endline (CicMetaSubst.ppsubst subst);
+      prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
+      assert false;
+    end;
+*)
+  let ty = apply_subst subst ty in
+  let left = apply_subst subst left in
+  let right = apply_subst subst right in
+  let fix_proof = function
     | NoProof -> NoProof 
-    | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
+    | BasicProof (subst',term) -> BasicProof (subst@subst',term)
     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
 	(*
 	let newsubst = 
           List.map
 	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
+	       let context = apply_subst_context subst context in
+	       let term = apply_subst subst term in
+	       let ty = apply_subst subst ty in  
 		 (i, (context, term, ty))) subst' in *)
           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
     | p -> assert false
@@ -1191,7 +1094,7 @@ let equality_of_term proof term =
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = compute_equality_weight stat in
-      let e = (w, BasicProof proof, stat, []) in
+      let e = (w, BasicProof ([],proof), stat, []) in
       e
   | _ ->
       raise TermIsNotAnEquality