- if t = t' then true
- else
- match t,t' with
- C.Rel _, C.Rel _
- | C.Var _, C.Var _
- | C.Meta _, C.Meta _
- | C.Sort _, C.Sort _
- | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
- | C.Cast (te,ty), C.Cast (te',ty') ->
- syntactic_equality te te' &&
- syntactic_equality ty ty'
- | C.Prod (n,s,t), C.Prod (n',s',t') ->
- n = n' &&
- syntactic_equality s s' &&
- syntactic_equality t t'
- | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
- n = n' &&
- syntactic_equality s s' &&
- syntactic_equality t t'
- | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
- n = n' &&
- syntactic_equality s s' &&
- syntactic_equality t t'
- | C.Appl l, C.Appl l' ->
- (try
- List.fold_left2
- (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
- with
- Invalid_argument _ -> false)
- | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
- | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
- UriManager.eq uri uri' && i = i'
- | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
- UriManager.eq uri uri' && i = i' && j = j'
- | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
- UriManager.eq sp sp' && i = i' &&
- syntactic_equality outt outt' &&
- syntactic_equality t t' &&
+ let rec aux t t' =
+ if t = t' then true
+ else
+ match t,t' with
+ C.Rel _, C.Rel _
+ | C.Var _, C.Var _
+ | C.Meta _, C.Meta _
+ | C.Sort _, C.Sort _
+ | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ | C.Cast (te,ty), C.Cast (te',ty') ->
+ aux te te' && aux ty ty'
+ | C.Prod (n,s,t), C.Prod (n',s',t') ->
+ (alpha_equivalence || n = n') && aux s s' && aux t t'
+ | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
+ (alpha_equivalence || n = n') && aux s s' && aux t t'
+ | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
+ (alpha_equivalence || n = n') && aux s s' && aux t t'
+ | C.Appl l, C.Appl l' ->
+ (try
+ List.fold_left2
+ (fun b t1 t2 -> b && aux t1 t2) true l l'
+ with
+ Invalid_argument _ -> false)
+ | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
+ | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
+ UriManager.eq uri uri' && i = i'
+ | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
+ UriManager.eq uri uri' && i = i' && j = j'
+ | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ UriManager.eq sp sp' && i = i' &&
+ aux outt outt' && aux t t' &&