Modifications to auto due to the introduction of the universe in

[helm.git] / components / tactics / paramodulation / equality.ml

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 7123c134a93a98056655f6cee83e55600b559945..10a64af19d09a15d762697512ba00de2270a964d 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -372,7 +372,8 @@ let contextualize uri ty left right t =
    * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
    * ctx_ty is the type of ctx
    *)
-    let rec aux uri ty left right ctx_d ctx_ty = function
+    let rec aux uri ty left right ctx_d ctx_ty t =
+      match t with 
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
         when LibraryObjects.is_sym_eq_URI uri_sym  ->
           let ty,l,r,p = open_sym ens tl in
@@ -407,8 +408,8 @@ let contextualize uri ty left right t =
           let c_what = put_in_ctx ctx_c what in
           (* now put the proofs in the compound context *)
           let p1 = (* p1: dc_what = d_m *)
-            if is_not_fixed_lp then 
-              aux uri ty2 c_what m ctx_d ctx_ty p1 
+            if is_not_fixed_lp then
+              aux uri ty2 c_what m ctx_d ctx_ty p1
             else
               mk_sym uri_sym ctx_ty d_m dc_what
                 (aux uri ty2 m c_what ctx_d ctx_ty p1)
@@ -417,7 +418,7 @@ let contextualize uri ty left right t =
             if avoid_eq_ind then
               mk_sym uri_sym ctx_ty dc_what dc_other
                 (aux uri ty1 what other ctx_dc ctx_ty p2)
-            else
+             else
               aux uri ty1 other what ctx_dc ctx_ty p2
           in
           (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
@@ -496,7 +497,7 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
     p
 ;;
 
-let parametrize_proof p l r ty = 
+let parametrize_proof menv p l r ty = 
   let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
   let mot = CicUtil.metas_of_term_set in
   let parameters = uniq (mot p @ mot l @ mot r) in 
@@ -517,9 +518,21 @@ let parametrize_proof p l r ty =
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
     ~what ~with_what ~where:p
   in
+  let ty_of_m _ = Cic.Implicit (Some `Type)
+(*
+  let ty_of_m = function
+    | Cic.Meta (i,_) ->
+       (try
+         let _,_,ty = CicUtil.lookup_meta i menv in ty
+       with CicUtil.Meta_not_found _ -> 
+         prerr_endline "eccoci";assert false)
+    | _ -> assert false
+*)
+  (*
   let ty_of_m _ = ty (*function 
     | Cic.Meta (i,_) -> List.assoc i menv 
     | _ -> assert false *)
+  *)
   in
   let args, proof,_ = 
     List.fold_left 
@@ -729,7 +742,7 @@ let build_goal_proof bag eq l initial ty se context menv =
         let p,l,r = proof_of_id bag id in
         let cic = build_proof_term bag eq h n p in
         let real_cic,instance = 
-          parametrize_proof cic l r (CicSubstitution.lift n mty)
+          parametrize_proof menv cic l r (CicSubstitution.lift n mty)
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h)