added entry "on the roles of mathml/latex"

[helm.git] / helm / ocaml / tactics / paramodulation / inference.ml

diff --git a/helm/ocaml/tactics/paramodulation/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml
index f22b49ceedfbb1e15345f37a1594b546a14a6a81..21dadc86870a36c4ed923a5fd14f6a72291a7de9 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/inference.ml
+++ b/helm/ocaml/tactics/paramodulation/inference.ml
@@ -500,7 +500,7 @@ let matching metasenv context t1 t2 ugraph =
 try
           unification metasenv context t1 t2 ugraph
 with CicUtil.Meta_not_found _ as exn ->
- Printf.eprintf "t1 = %s\nt2 = %s\nmetasenv = %s\n%!"
+ Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
   (CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv);
  raise exn
       in
@@ -910,12 +910,21 @@ let equality_of_term proof term =
 
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
+let is_weak_identity (metasenv, context, ugraph) = function
+  | (_, _, (ty, left, right, _), menv, _) -> 
+       (left = right ||
+          (meta_convertibility left right)) 
+          (* the test below is not a good idea since it stops
+             demodulation too early *)
+           (* (fst (CicReduction.are_convertible 
+                 ~metasenv:(metasenv @ menv) context left right ugraph)))*)
+;;
 
 let is_identity (metasenv, context, ugraph) = function
   | (_, _, (ty, left, right, _), menv, _) ->
        (left = right ||
-          (* (meta_convertibility left right) || *)
-          (fst (CicReduction.are_convertible 
+          (* (meta_convertibility left right)) *)
+           (fst (CicReduction.are_convertible 
                  ~metasenv:(metasenv @ menv) context left right ugraph)))
 ;;