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 f8e613723ff25eb69924d1e209f0bf14c258a2fb..e1bedeb207ff473653f1a06899b14df780b96c0d 100644 (file)
--- 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)