reverted previous fix

[helm.git] / components / tactics / proofEngineTypes.ml

diff --git a/components/tactics/proofEngineTypes.ml b/components/tactics/proofEngineTypes.ml
index b887c4bcd9a4ad03348d717d3c51dc4421be371e..abe460775b935a5271a6cda8a5deb8e1ac5a879f 100644 (file)
--- a/components/tactics/proofEngineTypes.ml
+++ b/components/tactics/proofEngineTypes.ml
@@ -28,12 +28,12 @@
   (**
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
-type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
+type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal
 
-let initial_status ty metasenv =
+let initial_status ty metasenv attrs =
   let rec aux max = function
     | [] -> max + 1
     | (idx, _, _) :: tl ->
@@ -43,8 +43,9 @@ let initial_status ty metasenv =
           aux max tl
   in
   let newmeta_idx = aux 0 metasenv in
+  let _subst = [] in
   let proof =
-    None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty
+    None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs
   in
   (proof, newmeta_idx)
 
@@ -90,13 +91,13 @@ exception Fail of string Lazy.t
     calls the opaque tactic on the status
   *)
 let apply_tactic t status = 
-  let (uri,metasenv,bo,ty), gl = t status in
+  let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
   match 
     CicRefine.pack_coercion_obj 
-      (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],[]))
+      (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
   with
-  | Cic.CurrentProof (_,metasenv,_,ty,_,_) -> 
-      (uri,metasenv,bo,ty), gl
+  | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) -> 
+      (uri,metasenv,subst,bo,ty, attrs), gl
   | _ -> assert false
 ;;
 
@@ -104,5 +105,5 @@ let apply_tactic t status =
 type mk_fresh_name_type =
  Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
 
-let goals_of_proof (_,metasenv,_,_) = List.map (fun (g,_,_) -> g) metasenv
+let goals_of_proof (_,metasenv,_subst,_,_,_) = List.map (fun (g,_,_) -> g) metasenv