X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=f13f35fbfb9c6552a621aada1db5aee60e40b1a9;hb=9c21f4a9a35415878189aca003847cbd42c1a9fc;hp=65c0b16138f3d5880006cb848e3f77a45b85f73d;hpb=21ee96d317a4f0e7abfe76f697defe78acc10b94;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 65c0b1613..f13f35fbf 100644
--- 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
   ;;