Support for the new auto tactics //

[helm.git] / helm / software / components / ng_paramodulation / nCicProof.ml

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 65c0b16138f3d5880006cb848e3f77a45b85f73d..1c74ac9e5b259d74fef23108a89aee864f88fb41 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -19,7 +19,7 @@ let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
        NCic.Const ref
   | EqInd_l -> 
@@ -31,7 +31,7 @@ let default_sig = function
       let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
        NCic.Const ref
   | Refl ->
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
        NCic.Const ref
 
@@ -68,7 +68,7 @@ let set_reference_of_oxuri reference_of_oxuri =
 (* let debug c r = prerr_endline r; c *)
 let debug c _ = c;;
 
-  let eqP() = debug (!eqsig Eq) "eqp"  ;;
+  let eqP() = debug (!eqsig Eq) "eq"  ;;
   let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
   let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";; 
   let eq_refl() = debug (!eqsig Refl) "refl";;
@@ -160,6 +160,10 @@ let debug c _ = c;;
          -> NCic.Appl [eq_refl();ty;l]
       | _ -> assert false
     in  
+    let proof_type =
+      let lit,_,_ = get_literal mp in
+      let lit = Subst.apply_subst subst lit in
+       extract 0 [] lit in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
@@ -239,6 +243,6 @@ let debug c _ = c;;
                  aux ongoal 
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
     in 
-      aux false [] steps
+      aux false [] steps, proof_type
   ;;