From 5fccdd2191e822f5ed140336bd15308e499d9dda Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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