bugfix on proof construction

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index a3dff3eb38bf4f94d00fee68d17805fd4ae9075e..197ceffbbbb6e06e48bd13cec42bba11eba34f34 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -1161,22 +1161,41 @@ let main dbd term metasenv ugraph =
         | ParamodulationFailure ->
             Printf.printf "NO proof found! :-(\n\n"
         | ParamodulationSuccess (Some goal, env) ->
-            let proof = Inference.build_proof_term goal in         
+            let proof = Inference.build_proof_term goal in
+(*             let proof = *)
+(* (\*               let p = CicSubstitution.lift 1 proof in *\) *)
+(*               let rec repl i = function *)
+(*                 | C.Meta _ -> C.Rel i *)
+(*                 | C.Appl l -> C.Appl (List.map (repl i) l) *)
+(*                 | C.Prod (n, s, t) -> C.Prod (n, s, repl (i+1) t) *)
+(*                 | C.Lambda (n, s, t) -> C.Lambda (n, s, repl (i+1) t) *)
+(*                 | t -> t *)
+(*               in *)
+(*               let p = repl 1 proof in *)
+(*               p *)
+(* (\*               C.Lambda (C.Anonymous, C.Rel 9, p) *\) *)
+(*             in *)
             let newmetasenv =
               List.fold_left
                 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
             in
             let _ =
+              Printf.printf "OK, found a proof!\n";
+              (* REMEMBER: we have to instantiate meta_proof, we should use
+                 apply  the "apply" tactic to proof and status 
+              *)
+              let names = names_of_context context in
+              print_endline (PP.pp proof names);
               try
                 let ty, ug =
                   CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
                 in
-                Printf.printf "OK, found a proof!\n";
-                (* REMEMBER: we have to instantiate meta_proof, we should use
-                   apply  the "apply" tactic to proof and status 
-                *)
-                let names = names_of_context context in
-                print_endline (PP.pp proof names);
+(*                 Printf.printf "OK, found a proof!\n"; *)
+(*                 (\* REMEMBER: we have to instantiate meta_proof, we should use *)
+(*                    apply  the "apply" tactic to proof and status  *)
+(*                 *\) *)
+(*                 let names = names_of_context context in *)
+(*                 print_endline (PP.pp proof names); *)
                 (*           print_endline (PP.ppterm proof); *)
                 
                 print_endline (string_of_float (finish -. start));