From 22ddac380a8574c0723b24f05c784d9a8690c736 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 11:35:30 +0000 Subject: [PATCH] A bit of renaming in the code to make it more clear. --- helm/ocaml/tactics/reductionTactics.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) 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' -- 2.39.2