status, (ctx, t)
;;
+let are_convertible status ctx a b =
+ let status, (_,a) = relocate status ctx a in
+ let status, (_,b) = relocate status ctx b in
+ let _n,_h,metasenv,subst,_o = status#obj in
+ let res = NCicReduction.are_convertible status metasenv subst ctx a b in
+ status, res
+;;
+let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;;
+
let unify status ctx a b =
let status, (_,a) = relocate status ctx a in
let status, (_,b) = relocate status ctx b in
let _,_,_,cl = List.nth tl i in
let consno = List.length cl in
let left, right = HExtlib.split_nth lno args in
- status, (ref, consno, left, right)
+ status, (ref, consno, left, right, cl)
;;
let apply_subst status ctx t =
match e1,e2 with
| Constant (u1,a1),Constant (u2,a2) ->
let x = NUri.compare u1 u2 in
- if x = 0 then Pervasives.compare a1 a2 else x
- | e1,e2 -> Pervasives.compare e1 e2
+ if x = 0 then Stdlib.compare a1 a2 else x
+ | e1,e2 -> Stdlib.compare e1 e2
;;
module Ncic_termOT : Set.OrderedType with type t = cic_term =
struct
type t = cic_term
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT)