List.map (function None -> None | Some t -> Some (um_aux t)) l
in
C.Meta (i,l'))
- | C.Sort _ as t -> t
- | C.Implicit _ -> assert false
+ | C.Sort _
+ | C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
| C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
let ppterm subst term = CicPp.ppterm (apply_subst subst term)
-let ppterm_in_context subst term name_context =
+let ppterm_in_name_context subst term name_context =
CicPp.pp (apply_subst subst term) name_context
+let ppterm_in_context subst term context =
+ let name_context =
+ List.map (function None -> None | Some (n,_) -> Some n) context
+ in
+ ppterm_in_name_context subst term name_context
+
let ppcontext' ?(sep = "\n") subst context =
let separate s = if s = "" then "" else s ^ sep in
List.fold_right
match context_entry with
Some (n,Cic.Decl t) ->
sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
- (ppterm_in_context subst t name_context), (Some n)::name_context
+ (ppterm_in_name_context subst t name_context), (Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
(match ty with
None -> "_"
- | Some ty -> ppterm_in_context subst ty name_context)
- (ppterm_in_context subst bo name_context), (Some n)::name_context
+ | Some ty -> ppterm_in_name_context subst ty name_context)
+ (ppterm_in_name_context subst bo name_context), (Some n)::name_context
| None ->
sprintf "%s_ :? _" (separate i), None::name_context
) context ("",[])
(fun (idx, (c, t,_)) ->
let context,name_context = ppcontext' ~sep:"; " subst c in
sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_context subst t name_context))
+ (ppterm_in_name_context subst t name_context))
subst)
(*
Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
(fun (idx, (c, t, _)) ->
let context,name_context = ppcontext' ~sep:"; " [] c in
sprintf "%s |- ?%d:= %s" context idx
- (ppterm_in_context [] t name_context))
+ (ppterm_in_name_context [] t name_context))
subst)
;;
(fun (i, c, t) ->
let context,name_context = ppcontext' ~sep:"; " subst c in
sprintf "%s |- ?%d: %s" context i
- (ppterm_in_context subst t name_context))
+ (ppterm_in_name_context subst t name_context))
(List.filter
(fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))