X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=f8782b7aec13db70083d025a44258d1416d0cf21;hb=1bcae23ef41ad2110426eebd97671d27d09213a3;hp=cced961c0fa54b838d25940805971554818d5540;hpb=d3314de1ff7affc9c82b8b4b63453a36ce2bcf64;p=helm.git

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