X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineTypes.ml;h=c60b6fdc0080ae6fbbecfa238a2c215267d31c83;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=68ea561f97988aa81c1cd614d66476971c227111;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineTypes.ml b/helm/software/components/tactics/proofEngineTypes.ml
index 68ea561f9..c60b6fdc0 100644
--- a/helm/software/components/tactics/proofEngineTypes.ml
+++ b/helm/software/components/tactics/proofEngineTypes.ml
@@ -28,12 +28,13 @@
   (**
     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 Lazy.t * 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 +44,10 @@ 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, 
+    lazy (Cic.Meta (newmeta_idx, [])), ty, attrs
   in
   (proof, newmeta_idx)
 
@@ -75,27 +78,36 @@ type ('term, 'lazy_term) pattern =
 
 type lazy_pattern = (Cic.term, Cic.lazy_term) pattern
 
+let hole = Cic.Implicit (Some `Hole)
+
 let conclusion_pattern t =
   let t' = 
     match t with
     | None -> None
-    | Some t -> Some (fun _ m u -> t, m, u)
+    | Some t -> Some (const_lazy_term t)
   in
-  t',[],Some (Cic.Implicit (Some `Hole))
+  t',[], Some hole
 
   (** tactic failure *)
 exception Fail of string Lazy.t
 
   (** 
-    calls the opaque tactic on the status, restoring the original 
-    universe graph if the tactic Fails
+    calls the opaque tactic on the status
   *)
 let apply_tactic t status = 
-  t status
+  let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
+  match 
+    CicRefine.pack_coercion_obj 
+      (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
+  with
+  | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) -> 
+      (uri,metasenv,subst,bo,ty, attrs), gl
+  | _ -> assert false
+;;
 
   (** constraint: the returned value will always be constructed by Cic.Name **)
 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