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!
;;
let unfold ?what context where =
;;
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',_)
match t1,t2 with
Cic.Const (uri,_), Cic.Const (uri',_)
| Cic.Var (uri,_), Cic.Var (uri',_)
| Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
| Cic.Const _, _
| Cic.Var _, _ -> false
| 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
| _,_ ->
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
in
let appl he tl =
if tl = [] then he else Cic.Appl (he::tl) in