From 73993c770d613df679df63d8d3d89fc37c02ae09 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:12:41 +0000 Subject: [PATCH] Added ~with_cast to the change tactic. When with_cast is true, a cast is recorded in the lambda term. --- .../components/tactics/reductionTactics.ml | 16 ++++++++++++++-- .../components/tactics/reductionTactics.mli | 3 ++- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index 3afef8eed..9c39caa6f 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -135,7 +135,7 @@ exception NotConvertible reference variables that are local to the term that is going to be replaced. To fix this we should parse with_what in the context of the term(s) to be replaced. *) -let change_tac ~pattern with_what = +let change_tac ?(with_cast=false) ~pattern with_what = let change_tac ~pattern ~with_what (proof, goal) = let curi,metasenv,_subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in @@ -206,7 +206,19 @@ let change_tac ~pattern with_what = | _ as t -> t) metasenv in - (curi,metasenv',_subst,pbo,pty, attrs), [metano] + let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in + if with_cast then + let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in + let (newproof,_) = + let irl= CicMkImplicit.identity_relocation_list_for_metavariable context' + in + ProofEngineHelpers.subst_meta_in_proof + proof metano + (Cic.Cast (Cic.Meta(metano',irl),ty')) [metano',context',ty'] + in + newproof, [metano'] + else + proof,[goal] in mk_tactic (change_tac ~pattern ~with_what) diff --git a/helm/software/components/tactics/reductionTactics.mli b/helm/software/components/tactics/reductionTactics.mli index 62200df69..f04e7dcac 100644 --- a/helm/software/components/tactics/reductionTactics.mli +++ b/helm/software/components/tactics/reductionTactics.mli @@ -35,7 +35,8 @@ val unfold_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val change_tac: +val change_tac: + ?with_cast:bool -> pattern:ProofEngineTypes.lazy_pattern -> Cic.lazy_term -> ProofEngineTypes.tactic -- 2.39.2