1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to

[helm.git] / helm / ocaml / tactics / reductionTactics.ml

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index d34678e52cf95e426c917df1205ec9dd27100b54..1885e956cf36191dd74bf18d08264915bd41aacb 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -30,31 +30,35 @@ open ProofEngineTypes
 let reduction_tac ~reduction ~pattern (proof,goal) =
   let curi,metasenv,pbo,pty = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
-  let change where terms =
+  let change subst where terms =
    if terms = [] then where
    else
     let terms, terms' = 
       List.split (List.map (fun (context, t) -> t, reduction context t) terms)
     in
+    let where' =
      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
-      ~where:where in
-  let (selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
-  let ty' = change ty selected_ty in
+      ~where:where
+    in
+     CicMetaSubst.apply_subst subst where' in
+  let (subst,metasenv,ugraph,selected_context,selected_ty) =
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+    ~conjecture ~pattern in
+  let ty' = change subst ty selected_ty in
   let context' =
    List.fold_right2
     (fun entry selected_entry context' ->
       match entry,selected_entry with
          None,None -> None::context'
        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
-          let ty' = change ty selected_ty in
+          let ty' = change subst ty selected_ty in
            Some (name,Cic.Decl ty')::context'
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = change bo selected_bo in
+          let bo' = change subst bo selected_bo in
           let ty' =
            match ty,selected_ty with
               None,None -> None
-            | Some ty,Some selected_ty -> Some (change ty selected_ty)
+            | Some ty,Some selected_ty -> Some (change subst ty selected_ty)
             | _,_ -> assert false
           in
            Some (name,Cic.Def (bo',ty'))::context'
@@ -97,7 +101,7 @@ let change_tac ~pattern with_what  =
   let curi,metasenv,pbo,pty = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   let context_len = List.length context in
-  let change context'_len where terms =
+  let change subst context'_len where terms =
    if terms = [] then where
    else
     let terms, terms' = 
@@ -134,11 +138,15 @@ let change_tac ~pattern with_what  =
           else
            raise NotConvertible) terms)
     in
-     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
-      ~where:where in
-  let (selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
-  let ty' = change context_len ty selected_ty in
+     let where' =
+      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+       ~where:where
+     in
+      CicMetaSubst.apply_subst subst where' in
+  let (subst,metasenv,ugraph,selected_context,selected_ty) =
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
+    ~pattern in
+  let ty' = change subst context_len ty selected_ty in
   let context' =
    List.fold_right2
     (fun entry selected_entry context' ->
@@ -146,15 +154,15 @@ let change_tac ~pattern with_what  =
      match entry,selected_entry with
          None,None -> None::context'
        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
-          let ty' = change context'_len ty selected_ty in
+          let ty' = change subst context'_len ty selected_ty in
            Some (name,Cic.Decl ty')::context'
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = change context'_len bo selected_bo in
+          let bo' = change subst context'_len bo selected_bo in
           let ty' =
            match ty,selected_ty with
               None,None -> None
             | Some ty,Some selected_ty ->
-               Some (change context'_len ty selected_ty)
+               Some (change subst context'_len ty selected_ty)
             | _,_ -> assert false
           in
            Some (name,Cic.Def (bo',ty'))::context'