fixed LetIn proofs

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

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 272a8100337c082485a6935fe270d5d3a2c8827f..ab27f8a314b13e4b75cce13afbd272a7f9440475 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let _profiler = <:profiler<_profiler>>;;
+
 (* $Id$ *)
 
 open Utils;;
@@ -144,7 +146,7 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
         (lazy
            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
               (CicPp.ppterm t1) (CicPp.ppterm t2)));
-      raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
+      raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
     ) else
       if b then
         (* full unification *)
@@ -170,22 +172,24 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 
 exception MatchingFailure;;
 
-let matching1 metasenv1 metasenv2 context t1 t2 ugraph = 
+(** 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 matching metasenv1 metasenv2 context t1 t2 ugraph = 
   try 
     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
   with
-    CicUnification .UnificationFailure _ ->
+    CicUnification.UnificationFailure _ -> 
       raise MatchingFailure
 ;;
 
-let unification = unification_aux true 
+let unification m1 m2 c t1 t2 ug = 
+  try 
+    unification_aux true m1 m2 c t1 t2 ug
+  with exn -> 
+    raise exn
 ;;
 
-(** 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 matching = matching1;;
 
 let check_eq context msg eq =
   let w, proof, (eq_ty, left, right, order), metas = eq in
@@ -485,3 +489,4 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
+let get_stats () = <:show<Inference.>> ;;