From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 11:35:30 +0000 (+0000)
Subject: A bit of renaming in the code to make it more clear.
X-Git-Tag: PRE_GETTER_STORAGE~99
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22ddac380a8574c0723b24f05c784d9a8690c736;p=helm.git

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 af5edd160..ae99ecb33 100644
--- 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'