Trying to be faster

[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..f13f35fbfb9c6552a621aada1db5aee60e40b1a9 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -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
   ;;