let set_default_eqP() = eqPref := default_eqP
-module type NCicContext =
- sig
- val metasenv : NCic.metasenv
- val subst : NCic.substitution
- val context : NCic.context
- end
-
-module NCicBlob(C : NCicContext) : Terms.Blob
+let saturate status metasenv subst context t ty =
+ let sty, _, args =
+ (* CSC: NCicPp.status is the best I can put here *)
+ NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0
+ in
+ let proof =
+ if args = [] then t
+ else NCic.Appl (t :: args)
+ in
+ proof, sty
+;;
+
+
+module NCicBlob: Terms.Blob
with type t = NCic.term and type input = NCic.term = struct
type t = NCic.term
let pp t =
(* CSC: NCicPp.status is the best I can put here *)
- (* WR: and I can't guess a user id, so I must put None *)
- (new NCicPp.status None)#ppterm ~context:C.context
- ~metasenv:C.metasenv ~subst:C.subst t;;
+ (new NCicPp.status None)#ppterm ~context:[] ~metasenv:[] ~subst:[] t
type input = NCic.term
let embed t = fst (embed t) ;;
- let saturate t ty =
- let sty, _, args =
- (* CSC: NCicPp.status is the best I can put here *)
- (* WR: and I can't guess a user id, so I must put None *)
- NCicMetaSubst.saturate (new NCicPp.status None) ~delta:0 C.metasenv C.subst
- C.context ty 0
- in
- let proof =
- if args = [] then Terms.Leaf t
- else Terms.Node (Terms.Leaf t :: List.map embed args)
- in
- let sty = embed sty in
- proof, sty
- ;;
-
end