From f3e1cddb1513c14530f1849477b6f5d0090b88cf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2005 12:17:15 +0000 Subject: [PATCH] Improvement/bug fix: rewriting in the hypothesis used to simplify the new hypothesis. This is no longer done. --- helm/ocaml/tactics/equalityTactics.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index b603bff9e..7ed946170 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -54,7 +54,7 @@ let rec rewrite_tac ~direction ~pattern equality = | _ -> let arg,dir2,tac,concl_pat,gty = match hyps_pat with - [] -> None,true,PT.exact_tac,concl_pat,gty + [] -> None,true,(fun ~term _ -> PT.exact_tac term),concl_pat,gty | [name,pat] -> let rec find_hyp n = function @@ -74,16 +74,17 @@ let rec rewrite_tac ~direction ~pattern equality = in let dummy = "dummy" in Some arg,false, - (fun ~term -> + (fun ~term typ -> Tacticals.seq ~tactics: [ProofEngineStructuralRules.rename name dummy; PT.letin_tac ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term; ProofEngineStructuralRules.clearbody name; - ReductionTactics.simpl_tac + ReductionTactics.change_tac ~pattern: - (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None); + (None,[name,Cic.Implicit (Some `Hole)],Cic.Implicit None) + (ProofEngineTypes.const_lazy_term typ); ProofEngineStructuralRules.clear dummy ]), pat,gty @@ -153,23 +154,24 @@ let rec rewrite_tac ~direction ~pattern equality = let pred = C.Lambda (fresh_name, ty, abstr_gty) in (* The argument is either a meta if we are rewriting in the conclusion or the hypothesis if we are rewriting in an hypothesis *) - let metasenv',arg = + let metasenv',arg,newtyp = match arg with None -> let gty' = CicSubstitution.subst t2 abstr_gty in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,gty')::metasenv' in - metasenv', C.Meta (fresh_meta,irl) + metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *) | Some arg -> - metasenv,arg + let gty' = CicSubstitution.subst t1 abstr_gty in + metasenv,arg,gty' in let exact_proof = C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality] in let (proof',goals) = PET.apply_tactic - (tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal) + (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal) in let goals = goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv -- 2.39.2