let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
let wrap_exc msg = function
| NCicUnification.Uncertain _ -> Uncertain msg
| NCicUnification.UnificationFailure _ -> RefineFailure msg
let wrap_exc msg = function
| NCicUnification.Uncertain _ -> Uncertain msg
| NCicUnification.UnificationFailure _ -> RefineFailure msg
| `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
| `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
| `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
| `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
| `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
| `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
| `Vector ->
raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
"can only be used in argument position")))
| `Vector ->
raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
"can only be used in argument position")))
- (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in
+ (metanoouttype,([`Name "outtype"],context,outtype,metaoutsort))::subst in
let outtype = newouttype in
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let outtype = newouttype in
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let rec first exc = function
| [] ->
raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
let rec first exc = function
| [] ->
raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
(NCicPp.ppterm ~metasenv ~subst ~context t)
(NCicPp.ppterm ~metasenv ~subst ~context infty)
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
(NCicPp.ppterm ~metasenv ~subst ~context t)
(NCicPp.ppterm ~metasenv ~subst ~context infty)
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)