snapshot

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

diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml
index 8ffde4bdf14569fb22706538151d3554c3af77ec..5830b08428729f3f1ca5143aee03dda67a129259 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/indexing.ml
+++ b/helm/ocaml/tactics/paramodulation/indexing.ml
@@ -32,6 +32,25 @@ module Index = Equality_indexing.DT (* path tree based indexing *)
 
 let debug_print = Utils.debug_print;;
 
+(* 
+for debugging 
+let check_equation env equation msg =
+  let w, proof, (eq_ty, left, right, order), metas, args = equation in
+  let metasenv, context, ugraph = env in
+  let metasenv' = metasenv @ metas in
+    try
+      CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+      CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+      ()
+    with 
+       CicUtil.Meta_not_found _ as exn ->
+         begin
+           prerr_endline msg; 
+           prerr_endline (CicPp.ppterm left);
+           prerr_endline (CicPp.ppterm right);
+           raise exn
+         end 
+*)
 
 type retrieval_mode = Matching | Unification;;
 
@@ -530,7 +549,10 @@ let rec demodulation_equality newmeta env table sign target =
          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
     in
     let left, right = if is_left then newterm, right else left, newterm in
-    let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
+    let m = 
+      (Inference.metas_of_term left) 
+      @ (Inference.metas_of_term right) 
+      @ (Inference.metas_of_term eq_ty) in
     (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
     and newargs = args
@@ -726,7 +748,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
+  let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
   let expansions, _ =
     let term = if ordering = U.Gt then left else right in
     betaexpand_term metasenv context ugraph table 0 term
@@ -800,7 +822,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 
     let res =
       let w = Utils.compute_equality_weight eq_ty left right in
-      (w, newproof, (eq_ty, left, right, neworder), [], [])
+      (w, newproof, (eq_ty, left, right, neworder), menv @ menv', [])
     in
     res
   in