Unfold tactic generalized to perform zeta-reduction.

WARNING: the tactic is bugged since it tries to zeta-expand a term that lives
in the context of the goal, not in the context of the pattern!

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index cced961c0fa54b838d25940805971554818d5540..f8782b7aec13db70083d025a44258d1416d0cf21 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -893,7 +893,8 @@ let simpl context =
 ;;
 
 let unfold ?what context where =
- let first_is_the_expandable_head_of_second t1 t2 =
+ let contextlen = List.length context in
+ let first_is_the_expandable_head_of_second context' t1 t2 =
   match t1,t2 with
      Cic.Const (uri,_), Cic.Const (uri',_)
    | Cic.Var (uri,_), Cic.Var (uri',_)
@@ -901,10 +902,14 @@ let unfold ?what context where =
    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
    | Cic.Const _, _
    | Cic.Var _, _ -> false
+   | Cic.Rel n, Cic.Rel m
+   | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
+      n + (List.length context' - contextlen) = m
+   | Cic.Rel _, _ -> false
    | _,_ ->
      raise
       (ProofEngineTypes.Fail
-        "The term to unfold is neither a constant nor a variable")
+        "The term to unfold is not a constant, a variable or a bound variable ")
  in
  let appl he tl =
   if tl = [] then he else Cic.Appl (he::tl) in