From 5fccdd2191e822f5ed140336bd15308e499d9dda Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 15:51:07 +0000 Subject: [PATCH] Bad hack to avoid failure of conversion (unfolding) in "unfold t in H" where H is a definition. In this case it is perfectly normal that t may not occur in the type or in the body of H. --- helm/software/components/tactics/reductionTactics.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index f8e613723..e1bedeb20 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -102,7 +102,17 @@ let unfold_tac what ~pattern = | Some lazy_term -> (fun context metasenv ugraph -> let what, metasenv, ugraph = lazy_term context metasenv ugraph in - ProofEngineReduction.unfold ~what, metasenv, ugraph) + let unfold ctx t = + try + ProofEngineReduction.unfold ~what ctx t + with + (* Not what we would like to have; however, this is required + right now for the case of a definition in the context: + if it works only in the body (or only in the type), that should + be accepted *) + ProofEngineTypes.Fail _ -> t + in + unfold, metasenv, ugraph) in mk_tactic (reduction_tac ~reduction ~pattern) -- 2.39.2