- match ty with
- | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r] when NUri.name_of_uri u = "eq" ->
- (let status, kind = classify ~subst:(get_subst status) ctx_ty l r in
- match kind with
- | `Identity ->
- let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
- status, Some (List.length ctx - i), kind
- | `Cycle | `Blob -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
- | _ ->
- if (List.for_all (fun x -> x <> n) acc) then
- status, Some (List.length ctx - i), kind
- else aux (i+1))
- | _ -> aux (i+1))
+ let status, kind = match ty with
+ | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r]
+ when NUri.name_of_uri u = "eq" ->
+ classify ~subst:(get_subst status) ctx_ty l r
+ | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;lty;l;rty;r]
+ when NUri.name_of_uri u = "jmeq" &&
+ NCicReduction.are_convertible ~metasenv:[]
+ ~subst:(get_subst status) ctx_ty lty rty
+ -> classify ~subst:(get_subst status) ctx_ty l r
+ | _ -> status, `NonEq
+ in match kind with
+ | `Identity ->
+ let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+ status, Some (List.length ctx - i), kind
+ | `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
+ | _ ->
+ if (List.for_all (fun x -> x <> n) acc) then
+ status, Some (List.length ctx - i), kind
+ else aux (i+1))