X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=16cff94d7796493f52a05658332a8261f564be4f;hb=7278063faf0ebb5fd08af2191989a12e2a27f522;hp=1398424353462320e130403a5bbc0a325d4d8e6b;hpb=e9e509ec3741689e5df17cc82662dad4a17e9eab;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 139842435..16cff94d7 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -246,14 +246,14 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_with_subst ~term ~subst (proof, goal) =
+let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = CicMkImplicit.new_meta metasenv subst in
+  let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -321,16 +321,17 @@ let apply_with_subst ~term ~subst (proof, goal) =
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
      newmetasenv''
    in
-   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
-    (newproof, 
-     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   subst,
+   (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+   max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
 
 
 (* ALB *)
-let apply_with_subst ~term ?(subst=[]) status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_with_subst ~term ~subst status
+    apply_with_subst ~term ~subst ~maxmeta status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
@@ -339,7 +340,7 @@ let apply_with_subst ~term ?(subst=[]) status =
 
 (* ALB *)
 let apply_tac_verbose ~term status =
-  let subst, status = apply_with_subst ~term status in
+  let subst, status, _ = apply_with_subst ~term status in
   (CicMetaSubst.apply_subst subst), status
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)