From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 16:48:46 +0000 (+0000)
Subject: Unfold tactic generalized to perform zeta-reduction.
X-Git-Tag: V_0_1_2_1~91
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8bbe4f30e98b4a1e0d51d17b64905461df669101;p=helm.git

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 cced961c0..f8782b7ae 100644
--- 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