A bit of renaming in the code to make it more clear.

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index af5edd160db47875e8604796969137e93e109fed..ae99ecb33d486be1f0069a9fce4b46f076b3a5f5 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -25,13 +25,14 @@
 
 open ProofEngineTypes
 
-(* The default of term is the thesis of the goal to be prooved *)
+(* Note: this code is almost identical to PrimitiveTactics.change_tac and
+*  it could be unified by making the change function a callback *)
 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 replace where terms =
+  let change where terms =
    if terms = [] then where
    else
     let terms, terms' = 
@@ -41,21 +42,21 @@ let reduction_tac ~reduction ~pattern
       ~where:where in
   let (selected_context,selected_ty) =
    ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
-  let ty' = replace ty selected_ty in
+  let ty' = change 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' = replace ty selected_ty in
+          let ty' = change ty selected_ty in
            Some (name,Cic.Decl ty')::context'
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = replace bo selected_bo in
+          let bo' = change bo selected_bo in
           let ty' =
            match ty,selected_ty with
               None,None -> None
-            | Some ty,Some selected_ty -> Some (replace ty selected_ty)
+            | Some ty,Some selected_ty -> Some (change ty selected_ty)
             | _,_ -> assert false
           in
            Some (name,Cic.Def (bo',ty'))::context'