From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Mar 2008 15:51:07 +0000 (+0000)
Subject: Bad hack to avoid failure of conversion (unfolding) in "unfold t in H" where
X-Git-Tag: make_still_working~5540
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fccdd2191e822f5ed140336bd15308e499d9dda;p=helm.git

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.
---

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)