X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=105b708e92d47d21c4b812d58876f405fe9347bd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e92117334acb7cf22964be509ca75d7887ea671b;hpb=febd89f8a2b61f958e149ed630f5c991eb7d9661;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index e92117334..105b708e9 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1,3 +1,28 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
 open Utils;;
 
 
@@ -16,11 +41,10 @@ and proof =
   | BasicProof of Cic.term
   | ProofBlock of
       Cic.substitution * UriManager.uri *
-        (* name, ty, eq_ty, left, right *)
-        (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * 
-        (Utils.pos * equality) * proof
-  | ProofGoalBlock of proof * equality
-  | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
+        (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
+  | ProofGoalBlock of proof * proof 
+  | ProofSymBlock of Cic.term list * proof
+  | SubProof of Cic.term * int * proof
 ;;
 
 
@@ -43,62 +67,59 @@ let string_of_equality ?env =
 ;;
 
 
-let build_proof_term equality =
-(*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
-(*   print_newline (); *)
+let rec string_of_proof = function
+  | NoProof -> "NoProof"
+  | BasicProof t -> "BasicProof " ^ (CicPp.ppterm 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 _ -> "ProofBlock"
+  | ProofGoalBlock (p1, p2) ->
+      Printf.sprintf "ProofGoalBlock(%s, %s)"
+        (string_of_proof p1) (string_of_proof p2)
+;;
+
+
+(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
+let build_ens_for_sym_eq sym_eq_URI termlist =
+  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+  match obj with
+  | Cic.Constant (_, _, _, uris, _) ->
+      assert (List.length uris <= List.length termlist);
+      let rec aux = function
+        | [], tl -> [], tl
+        | (uri::uris), (term::tl) ->
+            let ens, args = aux (uris, tl) in
+            (uri, term)::ens, args
+        | _, _ -> assert false
+      in
+      aux (uris, termlist)
+  | _ -> assert false
+;;
+
 
-  let indent = ref 0 in
-  
+let build_proof_term proof =
   let rec do_build_proof proof = 
     match proof with
     | NoProof ->
         Printf.fprintf stderr "WARNING: no proof!\n";
-(*           (string_of_equality equality); *)
         Cic.Implicit None
     | BasicProof term -> term
-    | ProofGoalBlock (proofbit, equality) ->
+    | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
-        let _, proof, _, _, _ = equality in
         do_build_goal_proof proofbit proof
-    | ProofSymBlock (ens, proof) ->
+    | ProofSymBlock (termlist, proof) ->
         let proof = do_build_proof proof in
-        Cic.Appl [
-          Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
-          proof
-        ]
-    | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
-(*         Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
-(*         print_newline (); *)
-
-        let name, ty, eq_ty, left, right = t' in
-        let bo =
-          Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
-                    eq_ty; left; right]
-        in
-        let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in
-        (*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
-        (*         (string_of_equality eq) (string_of_equality eq'); *)
-        (*       print_newline (); *)
-
-(*         let s = String.make !indent ' ' in *)
-(*         incr indent; *)
-        
-(*         print_endline (s ^ "build proof'------------"); *)
-        
+        let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
+        Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
+    | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
+        let t' = Cic.Lambda (name, ty, bo) in
         let proof' =
           let _, proof', _, _, _ = eq in
           do_build_proof proof'
         in
-(*         print_endline (s ^ "END proof'"); *)
-
-(*         print_endline (s ^ "build eqproof-----------"); *)
-
         let eqproof = do_build_proof eqproof in
-
-(*         print_endline (s ^ "END eqproof"); *)
-(*         decr indent; *)
-        
-        
         let _, _, (ty, what, other, _), menv', args' = eq in
         let what, other =
           if pos = Utils.Left then what, other else other, what
@@ -106,44 +127,33 @@ let build_proof_term equality =
         CicMetaSubst.apply_subst subst
           (Cic.Appl [Cic.Const (eq_URI, []); ty;
                      what; t'; eqproof; other; proof'])
+    | SubProof (term, meta_index, proof) ->
+        let proof = do_build_proof proof in
+        let eq i = function
+          | Cic.Meta (j, _) -> i = j
+          | _ -> false
+        in
+        ProofEngineReduction.replace
+          ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
 
   and do_build_goal_proof proofbit proof =
-(*     match proofbit with *)
-(*     | BasicProof _ -> do_build_proof proof *)
-(*     | proofbit -> *)
-        match proof with
-        | ProofGoalBlock (pb, eq) ->
-            do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
-(*             let _, proof, _, _, _  = eq in *)
-(*             let newproof = replace_proof proofbit proof in *)
-(*             do_build_proof newproof *)
-
-(*         | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
-(*             let eqproof' = replace_proof proofbit eqproof in *)
-(*             do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
-        | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
+    match proof with
+    | ProofGoalBlock (pb, p) ->
+        do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
+    | _ -> do_build_proof (replace_proof proofbit proof)
 
   and replace_proof newproof = function
-    | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
-        let uri = eq_URI in
-(*           if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
-(*             HelmLibraryObjects.Logic.eq_ind_r_URI *)
-(*           else *)
-(*             HelmLibraryObjects.Logic.eq_ind_URI *)
-(*         in *)
+    | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
         let eqproof' = replace_proof newproof eqproof in
-        ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
-(*         ProofBlock (subst, eq_URI, t', poseq, newproof) *)
-    | ProofGoalBlock (pb, equality) ->
+        ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
+    | ProofGoalBlock (pb, p) ->
         let pb' = replace_proof newproof pb in
-        ProofGoalBlock (pb', equality)
-(*         let w, proof, t, menv, args = equality in *)
-(*         let proof' = replace_proof newproof proof in *)
-(*         ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
+        ProofGoalBlock (pb', p)
     | BasicProof _ -> newproof
+    | SubProof (term, meta_index, p) ->
+        SubProof (term, meta_index, replace_proof newproof p)
     | p -> p
   in
-  let _, proof, _, _, _ = equality in
   do_build_proof proof
 ;;
 
@@ -185,9 +195,6 @@ let meta_convertibility_aux table t1 t2 =
          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
   in
   let rec aux ((table_l, table_r) as table) t1 t2 =
-(*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
-(*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
-(*       (print_table table_l) (print_table table_r); *)
     match t1, t2 with
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
         let m1_binding, table_l =
@@ -197,19 +204,6 @@ let meta_convertibility_aux table t1 t2 =
           try List.assoc m2 table_r, table_r
           with Not_found -> m1, (m2, m1)::table_r
         in
-(*         let m1_binding, m2_binding, table = *)
-(*           let m1b, table =  *)
-(*             try List.assoc m1 table, table *)
-(*             with Not_found -> m2, (m1, m2)::table *)
-(*           in *)
-(*           let m2b, table =  *)
-(*             try List.assoc m2 table, table *)
-(*             with Not_found -> m1, (m2, m1)::table *)
-(*           in *)
-(*           m1b, m2b, table *)
-(*         in *)
-(*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
-(*           (print_table table_l) (print_table table_r); *)
         if (m1_binding <> m2) || (m2_binding <> m1) then
           raise NotMetaConvertible
         else (
@@ -323,110 +317,12 @@ let meta_convertibility t1 t2 =
   else
     try
       let l, r = meta_convertibility_aux ([], []) t1 t2 in
-      (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
       true
     with NotMetaConvertible ->
       false
 ;;
 
 
-(*
-let replace_metas (* context *) term =
-  let module C = Cic in
-  let rec aux = function
-    | C.Meta (i, c) ->
-(*         let irl = *)
-(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
-(*         in *)
-(*         if c = irl then *)
-(*           C.Implicit (Some (`MetaIndex i)) *)
-(*         else ( *)
-(*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
-(*             (String.concat "\n" *)
-(*                (List.map *)
-(*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
-(*           C.Meta (i, c) *)
-(*         ) *)
-        C.Implicit (Some (`MetaInfo (i, c)))
-    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
-    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
-    | C.Cast (s, t) -> C.Cast (aux s, aux t)
-    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
-    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
-    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
-    | C.Appl l -> C.Appl (List.map aux l)
-    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
-    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
-    | C.MutCase (uri, i, s, t, l) ->
-        C.MutCase (uri, i, aux s, aux t, List.map aux l)
-    | C.Fix (i, il) ->
-        let il' =
-          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
-        C.Fix (i, il')
-    | C.CoFix (i, il) ->
-        let il' =
-          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
-        C.CoFix (i, il')
-    | t -> t
-  and aux_ens ens =
-    List.map (fun (u, t) -> (u, aux t)) ens
-  in
-  aux term
-;;
-*)
-
-
-(*
-let restore_metas (* context *) term =
-  let module C = Cic in
-  let rec aux = function
-    | C.Implicit (Some (`MetaInfo (i, c))) ->
-(*         let c = *)
-(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
-(*         in *)
-(*         C.Meta (i, c) *)
-(*         let local_context:(C.term option) list = *)
-(*           Marshal.from_string mc 0 *)
-(*         in *)
-(*         C.Meta (i, local_context) *)
-        C.Meta (i, c)
-    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
-    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
-    | C.Cast (s, t) -> C.Cast (aux s, aux t)
-    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
-    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
-    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
-    | C.Appl l -> C.Appl (List.map aux l)
-    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
-    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
-    | C.MutCase (uri, i, s, t, l) ->
-        C.MutCase (uri, i, aux s, aux t, List.map aux l)
-    | C.Fix (i, il) ->
-        let il' =
-          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
-        C.Fix (i, il')
-    | C.CoFix (i, il) ->
-        let il' =
-          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
-        C.CoFix (i, il')
-    | t -> t
-  and aux_ens ens =
-    List.map (fun (u, t) -> (u, aux t)) ens
-  in
-  aux term
-;;
-*)
-
-(*
-let rec restore_subst (* context *) subst =
-  List.map
-    (fun (i, (c, t, ty)) ->
-       i, (c, restore_metas (* context *) t, ty))
-    subst
-;;
-*)
-
-
 let rec check_irl start = function
   | [] -> true
   | None::tl -> check_irl (start+1) tl
@@ -435,6 +331,7 @@ let rec check_irl start = function
   | _ -> false
 ;;
 
+
 let rec is_simple_term = function
   | Cic.Appl ((Cic.Meta _)::_) -> false
   | Cic.Appl l -> List.for_all is_simple_term l
@@ -480,7 +377,8 @@ let unification_simple metasenv context t1 t2 ugraph =
     | C.Meta (i, _), C.Meta (j, _) when i > j ->
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise
+          (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
@@ -492,24 +390,26 @@ let unification_simple metasenv context t1 t2 ugraph =
           subst, menv
         with CicUtil.Meta_not_found m ->
           let names = names_of_context context in
-          debug_print (
-            Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
-              (CicPp.pp t1 names) (CicPp.pp t2 names)
-              (print_metasenv menv) (print_metasenv metasenv));
+          debug_print
+            (lazy
+               (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
+                  (CicPp.pp t1 names) (CicPp.pp t2 names)
+                  (print_metasenv menv) (print_metasenv metasenv)));
           assert false
       )
     | _, C.Meta _ -> unif subst menv t s
     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
         try
           List.fold_left2
             (fun (subst', menv) s t -> unif subst' menv s t)
             (subst, menv) tls tlt
         with Invalid_argument _ ->
-          raise (U.UnificationFailure "Inference.unification.unif")
+          raise (U.UnificationFailure (lazy "Inference.unification.unif"))
       )
-    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+    | _, _ ->
+        raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
   let menv =
@@ -524,12 +424,12 @@ let unification_simple metasenv context t1 t2 ugraph =
 
 
 let unification metasenv context t1 t2 ugraph =
-(*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
   let subst, menv, ug =
     if not (is_simple_term t1) || not (is_simple_term t2) then (
-      debug_print (
-        Printf.sprintf "NOT SIMPLE TERMS: %s %s"
-          (CicPp.ppterm t1) (CicPp.ppterm t2));
+      debug_print
+        (lazy
+           (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+              (CicPp.ppterm t1) (CicPp.ppterm t2)));
       CicUnification.fo_unif metasenv context t1 t2 ugraph
     ) else
       unification_simple metasenv context t1 t2 ugraph
@@ -545,17 +445,16 @@ let unification metasenv context t1 t2 ugraph =
     | [] -> []
     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
   in
-(*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
-(*   print_endline "|"; *)
   fix_subst subst, menv, ug
 ;;
 
 
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
 
 exception MatchingFailure;;
 
 
+(*
 let matching_simple metasenv context t1 t2 ugraph =
   let module C = Cic in
   let module M = CicMetaSubst in
@@ -569,22 +468,8 @@ let matching_simple metasenv context t1 t2 ugraph =
     | _ -> assert false
   in
   let rec do_match subst menv s t =
-(*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
-(*       (print_subst subst); *)
-(*     print_newline (); *)
-(*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
-(*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
-    (*       Printf.printf "after apply_subst: %s %s\n%s" *)
-    (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
-    (*       print_newline (); *)
     match s, t with
     | s, t when s = t -> subst, menv
-(*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
-(*         do_match subst menv t s *)
-(*     | C.Meta _, t when occurs_check subst s t -> *)
-(*         raise MatchingFailure *)
-(*     | s, C.Meta _ when occurs_check subst t s -> *)
-(*         raise MatchingFailure *)
     | s, C.Meta (i, l) ->
         let filter_menv i menv =
           List.filter (fun (m, _, _) -> i <> m) menv
@@ -592,8 +477,6 @@ let matching_simple metasenv context t1 t2 ugraph =
         let subst, menv =
           let value = lookup t subst in
           match value with
-(*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
-(*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
           | value when value = t ->
               let _, _, ty = CicUtil.lookup_meta i menv in
               (i, (context, s, ty))::subst, filter_menv i menv
@@ -602,54 +485,26 @@ let matching_simple metasenv context t1 t2 ugraph =
           | value -> do_match subst menv s value
         in
         subst, menv
-(*           else if value <> s then *)
-(*             raise MatchingFailure *)
-(*           else subst *)
-(*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
-(*           else subst *)
-(*         in *)
-(*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
-(*         subst, menv *)
-(*     | _, C.Meta _ -> do_match subst menv t s *)
-(*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
-(*         raise MatchingFailure *)
     | 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 _ ->
-(*           print_endline (Printexc.to_string e); *)
-(*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
-(*           print_newline ();           *)
           raise MatchingFailure
       )
     | _, _ ->
-(*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
-(*         print_newline (); *)
         raise MatchingFailure
   in
   let subst, menv = do_match [] metasenv t1 t2 in
-  (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
-  (*     print_newline (); *)
   subst, menv, ugraph
 ;;
+*)
 
 
 let matching metasenv context t1 t2 ugraph =
-(*   if (is_simple_term t1) && (is_simple_term t2) then *)
-(*     let subst, menv, ug = *)
-(*       matching_simple metasenv context t1 t2 ugraph in *)
-(* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
-(* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
-(* (\*     print_newline (); *\) *)
-(*     subst, menv, ug *)
-(*   else *)
-(*   Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
-(*   print_newline (); *)
     try
       let subst, metasenv, ugraph =
-        (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
         unification metasenv context t1 t2 ugraph
       in
       let t' = CicMetaSubst.apply_subst subst t1 in
@@ -663,385 +518,19 @@ let matching metasenv context t1 t2 ugraph =
           | s -> s
         in
         let subst = List.map fix_subst subst in
-
-(*         Printf.printf "matching %s %s:\n%s\n" *)
-(*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
-(*         print_newline (); *)
-
         subst, metasenv, ugraph
     with
     | CicUnification.UnificationFailure _
     | CicUnification.Uncertain _ ->
-(*       Printf.printf "failed to match %s %s\n" *)
-(*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
-(*       print_endline (Printexc.to_string e); *)
       raise MatchingFailure
 ;;
 
-(* let matching = *)
-(*   let profile = CicUtil.profile "Inference.matching" in *)
-(*   (fun metasenv context t1 t2 ugraph -> *)
-(*      profile (matching metasenv context t1 t2) ugraph) *)
-(* ;; *)
 
-
-let beta_expand ?(metas_ok=true) ?(match_only=false)
-    what type_of_what where context metasenv ugraph = 
-  let module S = CicSubstitution in
-  let module C = Cic in
-
-(*   let _ = *)
-(*     let names = names_of_context context in *)
-(*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
-(*       (CicPp.pp what names) (CicPp.ppterm what) *)
-(*       (CicPp.pp where names) (CicPp.ppterm where); *)
-(*     print_newline (); *)
-(*   in *)
-  (*
-    return value:
-    ((list of all possible beta expansions, subst, metasenv, ugraph),
-     lifted term)
-  *)
-  let rec aux lift_amount term context metasenv subst ugraph =
-(*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
-    let res, lifted_term = 
-      match term with
-      | C.Rel m  ->
-          [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
-            
-      | C.Var (uri, exp_named_subst) ->
-          let ens', lifted_ens =
-            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
-          in
-          let expansions = 
-            List.map
-              (fun (e, s, m, ug) ->
-                 (C.Var (uri, e), s, m, ug)) ens'
-          in
-          expansions, C.Var (uri, lifted_ens)
-            
-      | C.Meta (i, l) ->
-          let l', lifted_l = 
-            List.fold_right
-              (fun arg (res, lifted_tl) ->
-                 match arg with
-                 | Some arg ->
-                     let arg_res, lifted_arg =
-                       aux lift_amount arg context metasenv subst ugraph in
-                     let l1 =
-                       List.map
-                         (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
-                         arg_res
-                     in
-                     (l1 @
-                        (List.map
-                           (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
-                           res),
-                      (Some lifted_arg)::lifted_tl)
-                 | None ->
-                     (List.map
-                        (fun (r, s, m, ug) -> None::r, s, m, ug)
-                        res, 
-                      None::lifted_tl)
-              ) l ([], [])
-          in
-          let e = 
-            List.map
-              (fun (l, s, m, ug) ->
-                 (C.Meta (i, l), s, m, ug)) l'
-          in
-          e, C.Meta (i, lifted_l)
-            
-      | C.Sort _
-      | C.Implicit _ as t -> [], t
-          
-      | C.Cast (s, t) ->
-          let l1, lifted_s =
-            aux lift_amount s context metasenv subst ugraph in
-          let l2, lifted_t =
-            aux lift_amount t context metasenv subst ugraph
-          in
-          let l1' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.Cast (t, lifted_t), s, m, ug) l1 in
-          let l2' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.Cast (lifted_s, t), s, m, ug) l2 in
-          l1'@l2', C.Cast (lifted_s, lifted_t)
-            
-      | C.Prod (nn, s, t) ->
-          let l1, lifted_s =
-            aux lift_amount s context metasenv subst ugraph in
-          let l2, lifted_t =
-            aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
-              metasenv subst ugraph
-          in
-          let l1' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
-          let l2' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
-          l1'@l2', C.Prod (nn, lifted_s, lifted_t)
-
-      | C.Lambda (nn, s, t) ->
-          let l1, lifted_s =
-            aux lift_amount s context metasenv subst ugraph in
-          let l2, lifted_t =
-            aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
-              metasenv subst ugraph
-          in
-          let l1' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
-          let l2' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
-          l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
-
-      | C.LetIn (nn, s, t) ->
-          let l1, lifted_s =
-            aux lift_amount s context metasenv subst ugraph in
-          let l2, lifted_t =
-            aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
-              metasenv subst ugraph
-          in
-          let l1' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
-          let l2' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
-          l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
-
-      | C.Appl l ->
-          let l', lifted_l =
-            aux_list lift_amount l context metasenv subst ugraph
-          in
-          (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
-           C.Appl lifted_l)
-            
-      | C.Const (uri, exp_named_subst) ->
-          let ens', lifted_ens =
-            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
-          in
-          let expansions = 
-            List.map
-              (fun (e, s, m, ug) ->
-                 (C.Const (uri, e), s, m, ug)) ens'
-          in
-          (expansions, C.Const (uri, lifted_ens))
-
-      | C.MutInd (uri, i ,exp_named_subst) ->
-          let ens', lifted_ens =
-            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
-          in
-          let expansions = 
-            List.map
-              (fun (e, s, m, ug) ->
-                 (C.MutInd (uri, i, e), s, m, ug)) ens'
-          in
-          (expansions, C.MutInd (uri, i, lifted_ens))
-
-      | C.MutConstruct (uri, i, j, exp_named_subst) ->
-          let ens', lifted_ens =
-            aux_ens lift_amount exp_named_subst context metasenv subst ugraph
-          in
-          let expansions = 
-            List.map
-              (fun (e, s, m, ug) ->
-                 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
-          in
-          (expansions, C.MutConstruct (uri, i, j, lifted_ens))
-
-      | C.MutCase (sp, i, outt, t, pl) ->
-          let pl_res, lifted_pl =
-            aux_list lift_amount pl context metasenv subst ugraph
-          in
-          let l1, lifted_outt =
-            aux lift_amount outt context metasenv subst ugraph in
-          let l2, lifted_t =
-            aux lift_amount t context metasenv subst ugraph in
-
-          let l1' =
-            List.map
-              (fun (outt, s, m, ug) ->
-                 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
-          let l2' =
-            List.map
-              (fun (t, s, m, ug) ->
-                 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
-          let l3' =
-            List.map
-              (fun (pl, s, m, ug) ->
-                 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
-          in
-          (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
-
-      | C.Fix (i, fl) ->
-          let len = List.length fl in
-          let fl', lifted_fl =
-            List.fold_right
-              (fun (nm, idx, ty, bo) (res, lifted_tl) ->
-                 let lifted_ty = S.lift lift_amount ty in
-                 let bo_res, lifted_bo =
-                   aux (lift_amount+len) bo context metasenv subst ugraph in
-                 let l1 =
-                   List.map
-                     (fun (a, s, m, ug) ->
-                        (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
-                     bo_res
-                 in
-                 (l1 @
-                    (List.map
-                       (fun (r, s, m, ug) ->
-                          (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
-                  (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
-              ) fl ([], [])
-          in
-          (List.map
-             (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
-           C.Fix (i, lifted_fl))
-            
-      | C.CoFix (i, fl) ->
-          let len = List.length fl in
-          let fl', lifted_fl =
-            List.fold_right
-              (fun (nm, ty, bo) (res, lifted_tl) ->
-                 let lifted_ty = S.lift lift_amount ty in
-                 let bo_res, lifted_bo =
-                   aux (lift_amount+len) bo context metasenv subst ugraph in
-                 let l1 =
-                   List.map
-                     (fun (a, s, m, ug) ->
-                        (nm, lifted_ty, a)::lifted_tl, s, m, ug)
-                     bo_res
-                 in
-                 (l1 @
-                    (List.map
-                       (fun (r, s, m, ug) ->
-                          (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
-                  (nm, lifted_ty, lifted_bo)::lifted_tl)
-              ) fl ([], [])
-          in
-          (List.map
-             (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
-           C.CoFix (i, lifted_fl))
-    in
-    let retval = 
-      match term with
-      | C.Meta _ when (not metas_ok) ->
-          res, lifted_term
-      | _ ->
-(*           let term' = *)
-(*             if match_only then replace_metas context term *)
-(*             else term *)
-(*           in *)
-          try
-            let subst', metasenv', ugraph' =
-(*               Printf.printf "provo a unificare %s e %s\n" *)
-(*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
-              if match_only then
-                matching metasenv context term (S.lift lift_amount what) ugraph
-              else
-                CicUnification.fo_unif metasenv context
-                  (S.lift lift_amount what) term ugraph
-            in
-(*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
-(*             (CicPp.ppterm (S.lift lift_amount what)); *)
-(*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
-(*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
-            (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
-(*             if match_only then *)
-(*               let t' = CicMetaSubst.apply_subst subst' term in *)
-(*               if not (meta_convertibility term t') then ( *)
-(*                 res, lifted_term *)
-(*               ) else ( *)
-(*                 let metas = metas_of_term term in *)
-(*                 let fix_subst = function *)
-(*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
-(*                       (j, (c, C.Meta (i, lc), ty)) *)
-(*                   | s -> s *)
-(*                 in *)
-(*                 let subst' = List.map fix_subst subst' in *)
-(*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
-(*                  lifted_term) *)
-(*               ) *)
-(*             else *)
-              ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
-               lifted_term)
-          with
-          | MatchingFailure
-          | CicUnification.UnificationFailure _
-          | CicUnification.Uncertain _ ->
-              res, lifted_term
-    in
-(*     Printf.printf "exit aux\n"; *)
-    retval
-
-  and aux_list lift_amount l context metasenv subst ugraph =
-    List.fold_right
-      (fun arg (res, lifted_tl) ->
-         let arg_res, lifted_arg =
-           aux lift_amount arg context metasenv subst ugraph in
-         let l1 = List.map
-           (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
-         in
-         (l1 @ (List.map
-                  (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
-          lifted_arg::lifted_tl)
-      ) l ([], [])
-
-  and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
-    List.fold_right
-      (fun (u, arg) (res, lifted_tl) ->
-         let arg_res, lifted_arg =
-           aux lift_amount arg context metasenv subst ugraph in
-         let l1 =
-           List.map
-             (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
-         in
-         (l1 @ (List.map (fun (r, s, m, ug) ->
-                            (u, lifted_arg)::r, s, m, ug) res),
-          (u, lifted_arg)::lifted_tl)
-      ) exp_named_subst ([], [])
-
-  in
-  let expansions, _ =
-(*     let where = *)
-(*       if match_only then replace_metas (\* context *\) where *)
-(*       else where *)
-(*     in *)
-    aux 0 where context metasenv [] ugraph
-  in
-  let mapfun =
-(*     if match_only then *)
-(*       (fun (term, subst, metasenv, ugraph) -> *)
-(*          let term' = *)
-(*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
-(*          and subst = restore_subst subst in *)
-(*          (term', subst, metasenv, ugraph)) *)
-(*     else *)
-      (fun (term, subst, metasenv, ugraph) ->
-         let term' = C.Lambda (C.Anonymous, type_of_what, term) in
-         (term', subst, metasenv, ugraph))
-  in
-  List.map mapfun expansions
-;;
-
-
-let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
+let find_equalities context proof =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
+  let eq_uri = LibraryObjects.eq_URI () in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -1052,10 +541,9 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
         let do_find context term =
           match term with
           | C.Prod (name, s, t) ->
-(*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
               let (head, newmetas, args, newmeta) =
                 ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term)
+                  context (S.lift index term) 0
               in
               let p =
                 if List.length args = 0 then
@@ -1066,14 +554,9 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
-                    debug_print (
-                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
-(*                     debug_print ( *)
-(*                       Printf.sprintf "args: %s\n" *)
-(*                         (String.concat ", " (List.map CicPp.ppterm args))); *)
-(*                     debug_print ( *)
-(*                       Printf.sprintf "newmetas:\n%s\n" *)
-(*                         (print_metasenv newmetas)); *)
+                    debug_print
+                      (lazy
+                         (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1094,17 +577,20 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
           match do_find context term with
           | Some p, newmeta ->
               let tl, newmeta' = (aux (index+1) newmeta tl) in
-              p::tl, max newmeta newmeta'
+              (index, p)::tl, max newmeta newmeta'
           | None, _ ->
               aux (index+1) newmeta tl
         )
     | _::tl ->
         aux (index+1) newmeta tl
   in
-  aux 1 newmeta context
+  let il, maxm = aux 1 newmeta context in
+  let indexes, equalities = List.split il in
+  indexes, equalities, maxm
 ;;
 
 
+(*
 let equations_blacklist =
   List.fold_left
     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
@@ -1114,54 +600,95 @@ let equations_blacklist =
       "cic:/Coq/Init/Logic/f_equal.con";
       "cic:/Coq/Init/Logic/f_equal2.con";
       "cic:/Coq/Init/Logic/f_equal3.con";
+      "cic:/Coq/Init/Logic/f_equal4.con";
+      "cic:/Coq/Init/Logic/f_equal5.con";
       "cic:/Coq/Init/Logic/sym_eq.con";
-(*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
-(*       "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
-
+      "cic:/Coq/Init/Logic/eq_ind.con";
+      "cic:/Coq/Init/Logic/eq_ind_r.con";
+      "cic:/Coq/Init/Logic/eq_rec.con";
+      "cic:/Coq/Init/Logic/eq_rec_r.con";
+      "cic:/Coq/Init/Logic/eq_rect.con";
+      "cic:/Coq/Init/Logic/eq_rect_r.con";
+      "cic:/Coq/Logic/Eqdep/UIP.con";
+      "cic:/Coq/Logic/Eqdep/UIP_refl.con";
+      "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
+      "cic:/Coq/ZArith/Zcompare/rename.con";
       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
          perche' questo cacchio di teorema rompe le scatole :'( *)
-      "cic:/Rocq/SUBST/comparith/mult_n_2.con"; 
+      "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+
+      "cic:/matita/logic/equality/eq_f.con";
+      "cic:/matita/logic/equality/eq_f2.con";
+      "cic:/matita/logic/equality/eq_rec.con";
+      "cic:/matita/logic/equality/eq_rect.con";
     ]
 ;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
 
-let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = 
+let find_library_equalities dbd context status maxmeta = 
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
+  let blacklist =
+    List.fold_left
+      (fun s u -> UriManager.UriSet.add u s)
+      equations_blacklist
+      [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
+       eq_ind_r_URI ()]
+  in
   let candidates =
     List.fold_left
       (fun l uri ->
 	let suri = UriManager.string_of_uri uri in
-         if UriManager.UriSet.mem uri equations_blacklist then
+         if UriManager.UriSet.mem uri blacklist then
            l
          else
            let t = CicUtil.term_of_uri uri in
            let ty, _ =
              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
            in
-           (t, ty)::l)
+           (uri, t, ty)::l)
       []
-      (MetadataQuery.equations_for_goal ~dbd status)
+      (let t1 = Unix.gettimeofday () in
+       let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
+       let t2 = Unix.gettimeofday () in
+       (debug_print
+          (lazy
+             (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
+                (t2 -. t1))));
+       eqs)
   in
-  let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
-  and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
+  let eq_uri1 = eq_XURI ()
+  and eq_uri2 = LibraryObjects.eq_URI () in
   let iseq uri =
     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
   in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
   in
+  let rec has_vars = function
+    | C.Meta _ | C.Rel _ | C.Const _ -> false
+    | C.Var _ -> true
+    | C.Appl l -> List.exists has_vars l
+    | C.Prod (_, s, t) | C.Lambda (_, s, t)
+    | C.LetIn (_, s, t) | C.Cast (s, t) ->
+        (has_vars s) || (has_vars t)
+    | _ -> false
+  in
   let rec aux newmeta = function
     | [] -> [], newmeta
-    | (term, termty)::tl ->
-        debug_print (
-          Printf.sprintf "Examining: %s (%s)"
-            (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty));
+    | (uri, term, termty)::tl ->
+        debug_print
+          (lazy
+             (Printf.sprintf "Examining: %s (%s)"
+                (CicPp.ppterm term) (CicPp.ppterm termty)));
         let res, newmeta = 
           match termty with
-          | C.Prod (name, s, t) ->
+          | C.Prod (name, s, t) when not (has_vars termty) ->
               let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty
+                ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
               let p =
                 if List.length args = 0 then
@@ -1172,8 +699,9 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
                     when (iseq uri) && (ok_types ty newmetas) ->
-                    debug_print (
-                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
+                    debug_print
+                      (lazy
+                         (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1181,7 +709,8 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
-          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+              when iseq uri && not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
               let w = compute_equality_weight ty t1 t2 in
               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
@@ -1191,40 +720,98 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
         match res with
         | Some e ->
             let tl, newmeta' = aux newmeta tl in
-            e::tl, max newmeta newmeta'
+            (uri, e)::tl, max newmeta newmeta'
         | None ->
             aux newmeta tl
   in
   let found, maxm = aux maxmeta candidates in
-  (List.fold_left
-     (fun l e ->
-        if List.exists (meta_convertibility_eq e) l then (
-          debug_print (
-            Printf.sprintf "NO!! %s already there!" (string_of_equality e));
-          l
-        )
-        else e::l)
-     [] found), maxm
+  let uriset, eqlist = 
+    (List.fold_left
+       (fun (s, l) (u, e) ->
+          if List.exists (meta_convertibility_eq e) (List.map snd l) then (
+            debug_print
+              (lazy
+                 (Printf.sprintf "NO!! %s already there!"
+                    (string_of_equality e)));
+            (UriManager.UriSet.add u s, l)
+          ) else (UriManager.UriSet.add u s, (u, e)::l))
+       (UriManager.UriSet.empty, []) found)
+  in
+  uriset, eqlist, maxm
+;;
+
+
+let find_library_theorems dbd env status equalities_uris =
+  let module C = Cic in
+  let module S = CicSubstitution in
+  let module T = CicTypeChecker in
+  let blacklist =
+    let refl_equal =
+      UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
+    let s =
+      UriManager.UriSet.remove refl_equal
+        (UriManager.UriSet.union equalities_uris equations_blacklist)
+    in
+    List.fold_left
+      (fun s u -> UriManager.UriSet.add u s)
+      s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
+         eq_ind_r_URI ()]
+  in
+  let metasenv, context, ugraph = env in
+  let candidates =
+    List.fold_left
+      (fun l uri ->
+         if UriManager.UriSet.mem uri blacklist then l
+         else
+           let t = CicUtil.term_of_uri uri in
+           let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
+           (t, ty, [])::l)
+      [] (MetadataQuery.signature_of_goal ~dbd status)
+  in
+  let refl_equal =
+    let u = eq_XURI () in
+    let t = CicUtil.term_of_uri u in
+    let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+    (t, ty, [])
+  in
+  refl_equal::candidates
+;;
+
+
+let find_context_hypotheses env equalities_indexes =
+  let metasenv, context, ugraph = env in
+  let _, res = 
+    List.fold_left
+      (fun (n, l) entry ->
+         match entry with
+         | None -> (n+1, l)
+         | Some _ ->
+             if List.mem n equalities_indexes then
+               (n+1, l)
+             else
+               let t = Cic.Rel n in
+               let ty, _ =
+                 CicTypeChecker.type_of_aux' metasenv context t ugraph in 
+               (n+1, (t, ty, [])::l))
+      (1, []) context
+  in
+  res
 ;;
 
 
 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
-(*   print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
   let table = Hashtbl.create (List.length args) in
-  let is_this_case = ref false in
   let newargs, newmeta =
     List.fold_right
       (fun t (newargs, index) ->
          match t with
          | Cic.Meta (i, l) ->
-             Hashtbl.add table i index;
-(*              if index = 5469 then ( *)
-(*                Printf.printf "?5469 COMES FROM (%d): %s\n" *)
-(*                  i (string_of_equality equality); *)
-(*                print_newline (); *)
-(*                is_this_case := true *)
-(*              ); *)
-             ((Cic.Meta (index, l))::newargs, index+1)
+             if Hashtbl.mem table i then
+               let idx = Hashtbl.find table i in
+               ((Cic.Meta (idx, l))::newargs, index+1)
+             else
+               let _ = Hashtbl.add table i index in
+               ((Cic.Meta (index, l))::newargs, index+1)
          | _ -> assert false)
       args ([], newmeta+1)
   in
@@ -1246,19 +833,35 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
   and left = repl left
   and right = repl right in
   let metas = (metas_of_term left) @ (metas_of_term right) in
-  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
-  and newargs =
+  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
+  let newargs =
     List.filter
       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
+  let _ =
+    if List.length metas > 0 then 
+      let first = List.hd metas in
+      (* this new equality might have less variables than its parents: here
+         we fill the gap with a dummy arg. Example:
+         with (f X Y) = X we can simplify
+         (g X) = (f X Y) in
+         (g X) = X. 
+         So the new equation has only one variable, but it still has type like
+         \lambda X,Y:..., so we need to pass a dummy arg for Y
+         (I hope this makes some sense...)
+      *)
+      Hashtbl.iter
+        (fun k v ->
+           if not (List.exists
+                     (function Cic.Meta (i, _) -> i = v | _ -> assert false)
+                     newargs) then
+             Hashtbl.replace table k first)
+        (Hashtbl.copy table)
+  in
   let rec fix_proof = function
     | NoProof -> NoProof
     | BasicProof term -> BasicProof (repl term)
-    | ProofBlock (subst, eq_URI, t', (pos, eq), p) ->
-
-(*         Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
-(*           (string_of_equality equality) (print_subst subst); *)
-        
+    | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
         let subst' =
           List.fold_left
             (fun s arg ->
@@ -1269,47 +872,24 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
                      if List.mem_assoc i subst then
                        s
                      else
-(*                        let _, context, ty = CicUtil.lookup_meta j menv' in *)
-(*                        (i, (context, Cic.Meta (j, l), ty))::s *)
                        let _, context, ty = CicUtil.lookup_meta i menv in
                        (i, (context, Cic.Meta (j, l), ty))::s
-                   with Not_found -> s
+                   with Not_found | CicUtil.Meta_not_found _ ->
+                     s
                  )
                | _ -> assert false)
             [] args
         in
-(*         let subst'' = *)
-(*           List.map *)
-(*             (fun (i, e) -> *)
-(*                try let j = Hashtbl.find table i in (j, e) *)
-(*                with _ -> (i, e)) subst *)
-(*         in *)
-
-(*         Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
-(*         print_newline (); *)
-        
-        ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
-(*     | ProofSymBlock (ens, p) -> *)
-(*         let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
-(*         ProofSymBlock (ens', fix_proof p) *)
+        ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
     | p -> assert false
   in
-(*   (newmeta + (List.length newargs) + 2, *)
   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
-(*   if !is_this_case then ( *)
-(*     print_endline "\nTHIS IS THE TROUBLE!!!"; *)
-(*     let pt = build_proof_term neweq in *)
-(*     Printf.printf "equality: %s\nproof: %s\n" *)
-(*       (string_of_equality neweq) (CicPp.ppterm pt); *)
-(*     print_endline (String.make 79 '-'); *)
-(*   ); *)
   (newmeta + 1, neweq)
-(*    (w, fix_proof p, (ty, left, right, o), menv', newargs)) *)
 ;;
 
 
-let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
-  let iseq uri = UriManager.eq uri eq_uri in
+let term_is_equality term =
+  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
@@ -1318,7 +898,8 @@ let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
 
 exception TermIsNotAnEquality;;
 
-let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
+let equality_of_term proof term =
+  let eq_uri = LibraryObjects.eq_URI () in
   let iseq uri = UriManager.eq uri eq_uri in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
@@ -1326,7 +907,6 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
       let w = compute_equality_weight ty t1 t2 in
       let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
       e
-(*       (proof, (ty, t1, t2, o), [], []) *)
   | _ ->
       raise TermIsNotAnEquality
 ;;
@@ -1335,438 +915,10 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 
-(*
-let superposition_left (metasenv, context, ugraph) target source =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module M = CicMetaSubst in
-  let module HL = HelmLibraryObjects in
-  let module CR = CicReduction in
-  (* we assume that target is ground (does not contain metavariables): this
-   * should always be the case (I hope, at least) *)
-  let proof, (eq_ty, left, right, t_order), _, _ = target in
-  let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
-
-  let compare_terms = !Utils.compare_terms in
-
-  if eq_ty <> ty then
-    []
-  else    
-    let where, is_left =
-      match t_order (* compare_terms left right *) with
-      | Lt -> right, false
-      | Gt -> left, true
-      | _ -> (
-          Printf.printf "????????? %s = %s" (CicPp.ppterm left)
-            (CicPp.ppterm right);
-          print_newline ();
-          assert false (* again, for ground terms this shouldn't happen... *)
-        )
-    in
-    let metasenv' = newmetas @ metasenv in
-    let result = s_order (* compare_terms t1 t2 *) in
-    let res1, res2 = 
-      match result with
-      | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
-      | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
-      | _ ->
-          let res1 =
-            List.filter
-              (fun (t, s, m, ug) ->
-                 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
-              (beta_expand t1 ty where context metasenv' ugraph)
-          and res2 =
-            List.filter
-              (fun (t, s, m, ug) ->
-                 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
-              (beta_expand t2 ty where context metasenv' ugraph)
-          in
-          res1, res2
-    in
-    (*   let what, other = *)
-    (*     if is_left then left, right *)
-    (*     else right, left *)
-    (*   in *)
-    let build_new what other eq_URI (t, s, m, ug) =
-      let newgoal, newgoalproof =
-        match t with
-        | C.Lambda (nn, ty, bo) ->
-            let bo' = S.subst (M.apply_subst s other) bo in
-            let bo'' =
-              C.Appl (
-                [C.MutInd (HL.Logic.eq_URI, 0, []);
-                 S.lift 1 eq_ty] @
-                  if is_left then [bo'; S.lift 1 right]
-                  else [S.lift 1 left; bo'])
-            in
-            let t' = C.Lambda (nn, ty, bo'') in
-            S.subst (M.apply_subst s other) bo,
-            M.apply_subst s
-              (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                       proof; other; eqproof])
-        | _ -> assert false
-      in
-      let equation =
-        if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
-        else (eq_ty, left, newgoal, compare_terms left newgoal)
-      in
-      (newgoalproof (* eqproof *), equation, [], [])
-    in
-    let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
-    and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
-    new1 @ new2
-;;
-
-
-let superposition_right newmeta (metasenv, context, ugraph) target source =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module M = CicMetaSubst in
-  let module HL = HelmLibraryObjects in
-  let module CR = CicReduction in
-  let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
-  let eqp', (ty', t1, t2, s_order), newm', args' = source in
-  let maxmeta = ref newmeta in
-
-  let compare_terms = !Utils.compare_terms in
-
-  if eq_ty <> ty' then
-    newmeta, []
-  else
-    (*   let ok term subst other other_eq_side ugraph = *)
-    (*     match term with *)
-    (*     | C.Lambda (nn, ty, bo) -> *)
-    (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
-    (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
-    (*         not res *)
-    (*     |  _ -> assert false *)
-    (*   in *)
-    let condition left right what other (t, s, m, ug) =
-      let subst = M.apply_subst s in
-      let cmp1 = compare_terms (subst what) (subst other) in
-      let cmp2 = compare_terms (subst left) (subst right) in
-      (*     cmp1 = Gt && cmp2 = Gt *)
-      cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
-        (*     && (ok t s other right ug) *)
-    in
-    let metasenv' = metasenv @ newmetas @ newm' in
-    let beta_expand = beta_expand ~metas_ok:false in
-    let cmp1 = t_order (* compare_terms left right *)
-    and cmp2 = s_order (* compare_terms t1 t2 *) in
-    let res1, res2, res3, res4 =
-      let res l r s t =
-        List.filter
-          (condition l r s t)
-          (beta_expand s eq_ty l context metasenv' ugraph)
-      in
-      match cmp1, cmp2 with
-      | Gt, Gt ->
-          (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
-      | Gt, Lt ->
-          [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
-      | Lt, Gt ->
-          [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
-      | Lt, Lt ->
-          [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
-      | Gt, _ ->
-          let res1 = res left right t1 t2
-          and res2 = res left right t2 t1 in
-          res1, res2, [], []
-      | Lt, _ ->
-          let res3 = res right left t1 t2
-          and res4 = res right left t2 t1 in
-          [], [], res3, res4
-      | _, Gt ->
-          let res1 = res left right t1 t2
-          and res3 = res right left t1 t2 in
-          res1, [], res3, []
-      | _, Lt ->
-          let res2 = res left right t2 t1
-          and res4 = res right left t2 t1 in
-          [], res2, [], res4
-      | _, _ ->
-          let res1 = res left right t1 t2
-          and res2 = res left right t2 t1
-          and res3 = res right left t1 t2
-          and res4 = res right left t2 t1 in
-          res1, res2, res3, res4
-    in
-    let newmetas = newmetas @ newm' in
-    let newargs = args @ args' in
-    let build_new what other is_left eq_URI (t, s, m, ug) =
-      (*     let what, other = *)
-      (*       if is_left then left, right *)
-      (*       else right, left *)
-      (*     in *)
-      let newterm, neweqproof =
-        match t with
-        | C.Lambda (nn, ty, bo) ->
-            let bo' = M.apply_subst s (S.subst other bo) in
-            let bo'' =
-              C.Appl (
-                [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
-                  if is_left then [bo'; S.lift 1 right]
-                  else [S.lift 1 left; bo'])
-            in
-            let t' = C.Lambda (nn, ty, bo'') in
-            bo',
-            M.apply_subst s
-              (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                       eqproof; other; eqp'])
-        | _ -> assert false
-      in
-      let newmeta, newequality =
-        let left, right =
-          if is_left then (newterm, M.apply_subst s right)
-          else (M.apply_subst s left, newterm) in
-        let neworder = compare_terms left right in
-        fix_metas !maxmeta
-          (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
-      in
-      maxmeta := newmeta;
-      newequality
-    in
-    let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
-    and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
-    and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
-    and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
-    let ok = function
-      | _, (_, left, right, _), _, _ ->
-          not (fst (CR.are_convertible context left right ugraph))
-    in
-    (!maxmeta,
-     (List.filter ok (new1 @ new2 @ new3 @ new4)))
-;;
-*)
-
-
-let is_identity ((_, context, ugraph) as env) = function
-  | ((_, _, (ty, left, right, _), _, _) as equality) ->
+let is_identity ((metasenv, context, ugraph) as env) = function
+  | ((_, _, (ty, left, right, _), menv, _) as equality) ->
       (left = right ||
-          (fst (CicReduction.are_convertible context left right ugraph)))
-;;
-
-
-(*
-let demodulation newmeta (metasenv, context, ugraph) target source =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module M = CicMetaSubst in
-  let module HL = HelmLibraryObjects in
-  let module CR = CicReduction in
-
-  let proof, (eq_ty, left, right, t_order), metas, args = target
-  and proof', (ty, t1, t2, s_order), metas', args' = source in
-
-  let compare_terms = !Utils.compare_terms in
-  
-  if eq_ty <> ty then
-    newmeta, target
-  else
-    let first_step, get_params = 
-      match s_order (* compare_terms t1 t2 *) with
-      | Gt -> 1, (function
-                    | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
-                    | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
-                    | _ -> assert false)
-      | Lt -> 1, (function
-                    | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
-                    | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
-                    | _ -> assert false)
-      | _ ->
-          let first_step = 3 in
-          let get_params step =
-            match step with
-            | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
-            | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
-            | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
-            | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
-            | _ -> assert false
-          in
-          first_step, get_params
-    in
-    let rec demodulate newmeta step metasenv target =
-      let proof, (eq_ty, left, right, t_order), metas, args = target in
-      let is_left, what, other, eq_URI = get_params step in
-
-      let env = metasenv, context, ugraph in
-      let names = names_of_context context in
-(*       Printf.printf *)
-(*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(*         (string_of_equality ~env target) (CicPp.pp what names) *)
-(*         (CicPp.pp other names) (string_of_bool is_left); *)
-(*       Printf.printf "step: %d" step; *)
-(*       print_newline (); *)
-
-      let ok (t, s, m, ug) =
-        compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
-      in
-      let res =
-        let r = (beta_expand ~metas_ok:false ~match_only:true
-                   what ty (if is_left then left else right)
-                   context (metasenv @ metas) ugraph) 
-        in
-(*         let m' = metas_of_term what *)
-(*         and m'' = metas_of_term (if is_left then left else right) in *)
-(*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
-(*           Printf.printf *)
-(*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(*             (string_of_equality ~env target) (CicPp.pp what names) *)
-(*             (CicPp.pp other names) (string_of_bool is_left); *)
-(*           Printf.printf "step: %d" step; *)
-(*           print_newline (); *)
-(*           print_endline "res:"; *)
-(*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
-(*           print_newline (); *)
-(*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
-(*           print_newline (); *)
-(*         ); *)
-        List.filter ok r
-      in
-      match res with
-      | [] ->
-          if step = 0 then newmeta, target
-          else demodulate newmeta (step-1) metasenv target
-      | (t, s, m, ug)::_ -> 
-          let newterm, newproof =
-            match t with
-            | C.Lambda (nn, ty, bo) ->
-(*                 let bo' = M.apply_subst s (S.subst other bo) in *)
-                let bo' = S.subst (M.apply_subst s other) bo in
-                let bo'' =
-                  C.Appl (
-                    [C.MutInd (HL.Logic.eq_URI, 0, []);
-                     S.lift 1 eq_ty] @
-                      if is_left then [bo'; S.lift 1 right]
-                      else [S.lift 1 left; bo'])
-                in
-                let t' = C.Lambda (nn, ty, bo'') in
-(*                 M.apply_subst s (S.subst other bo), *)
-                bo', 
-                M.apply_subst s
-                  (C.Appl [C.Const (eq_URI, []); ty; what; t';
-                           proof; other; proof'])
-            | _ -> assert false
-          in
-          let newmeta, newtarget =
-            let left, right =
-(*               if is_left then (newterm, M.apply_subst s right) *)
-(*               else (M.apply_subst s left, newterm) in *)
-              if is_left then newterm, right
-              else left, newterm
-            in
-            let neworder = compare_terms left right in
-(*             let newmetasenv = metasenv @ metas in *)
-(*             let newargs = args @ args' in *)
-(*             fix_metas newmeta *)
-(*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
-            let m = (metas_of_term left) @ (metas_of_term right) in
-            let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
-            and newargs =
-              List.filter
-                (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
-                args
-            in
-            newmeta,
-            (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
-          in
-(*           Printf.printf *)
-(*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
-(*             (string_of_equality ~env newtarget) *)
-(*             (string_of_equality ~env target); *)
-(* (\*           let _, _, newm, newa = newtarget in *\) *)
-(* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
-(* (\*             (print_metasenv newm) *\) *)
-(* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
-(*           print_newline (); *)
-          if is_identity env newtarget then
-            newmeta, newtarget
-          else
-            demodulate newmeta first_step metasenv newtarget
-    in
-    demodulate newmeta first_step (metasenv @ metas') target
+          (* (meta_convertibility left right) || *)
+          (fst (CicReduction.are_convertible 
+		  ~metasenv:(metasenv @ menv) context left right ugraph)))
 ;;
-
-
-(*
-let demodulation newmeta env target source =
-  newmeta, target
-;;
-*)
-
-
-let subsumption env target source =
-  let _, (ty, tl, tr, _), tmetas, _ = target
-  and _, (ty', sl, sr, _), smetas, _ = source in
-  if ty <> ty' then
-    false
-  else
-    let metasenv, context, ugraph = env in
-    let metasenv = metasenv @ tmetas @ smetas in
-    let names = names_of_context context in
-    let samesubst subst subst' =
-(*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
-(*         (print_subst subst) (print_subst subst'); *)
-(*       print_newline (); *)
-      let tbl = Hashtbl.create (List.length subst) in
-      List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
-      List.for_all
-        (fun (m, (c, t1, t2)) ->
-           try
-             let c', t1', t2' = Hashtbl.find tbl m in
-             if (c = c') && (t1 = t1') && (t2 = t2') then true
-             else false
-           with Not_found ->
-             true)
-        subst'
-    in
-    let subsaux left right left' right' =
-      try
-        let subst, menv, ug = matching metasenv context left left' ugraph
-        and subst', menv', ug' = matching metasenv context right right' ugraph
-        in
-(*         Printf.printf "left = right: %s = %s\n" *)
-(*           (CicPp.pp left names) (CicPp.pp right names); *)
-(*         Printf.printf "left' = right': %s = %s\n" *)
-(*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
-        samesubst subst subst'
-      with e ->
-(*         print_endline (Printexc.to_string e); *)
-        false
-    in
-    let res = 
-      if subsaux tl tr sl sr then true
-      else subsaux tl tr sr sl
-    in
-    if res then (
-      Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
-        (string_of_equality ~env target) (string_of_equality ~env source);
-      print_newline ();
-    );
-    res
-;;
-*)
-
-
-let extract_differing_subterms t1 t2 =
-  let module C = Cic in
-  let rec aux t1 t2 =
-    match t1, t2 with
-    | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
-        [(t1, t2)]
-    | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
-        let res = List.concat (List.map2 aux tl1 tl2) in
-        if h1 <> h2 then
-          if res = [] then [(h1, h2)] else [(t1, t2)]
-        else
-          if List.length res > 1 then [(t1, t2)] else res
-    | t1, t2 ->
-        if t1 <> t2 then [(t1, t2)] else []
-  in
-  let res = aux t1 t2 in
-  match res with
-  | hd::[] -> Some hd
-  | _ -> None
-;;
-
-