diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 36 |
1 files changed, 27 insertions, 9 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c8ecf91d3..67a8f01aa 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -24,6 +24,7 @@ open Nametab open Mod_subst open Misctypes open Decl_kinds +open Context.Named.Declaration let dl = Loc.ghost @@ -33,8 +34,15 @@ let print_universes = Flags.univ_print (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false -let add_name na b t (nenv, env) = add_name na nenv, push_rel (na, b, t) env -let add_name_opt na b t (nenv, env) = +let add_name na b t (nenv, env) = + let open Context.Rel.Declaration in + add_name na nenv, push_rel (match b with + | None -> LocalAssum (na,t) + | Some b -> LocalDef (na,b,t) + ) + env + +let add_name_opt na b t (nenv, env) = match t with | None -> Termops.add_name na nenv, env | Some t -> add_name na b t (nenv, env) @@ -510,11 +518,14 @@ let rec detype flags avoid env sigma t = else noparams () | Evar (evk,cl) -> - let bound_to_itself_or_letin (id,b,_) c = - b != None || - try let n = List.index Name.equal (Name id) (fst env) in - isRelN n c - with Not_found -> isVarId id c in + let bound_to_itself_or_letin decl c = + match decl with + | LocalDef _ -> true + | LocalAssum (id,_) -> + try let n = List.index Name.equal (Name id) (fst env) in + isRelN n c + with Not_found -> isVarId id c + in let id,l = try let id = Evd.evar_ident evk sigma in @@ -684,17 +695,24 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] - | (na,b,t)::rest -> + | decl::rest -> + let open Context.Rel.Declaration in + let na = get_name decl in + let t = get_type decl in let na',avoid' = match where with | None -> na,avoid | Some c -> - if b != None then + if is_local_def decl then compute_displayed_let_name_in (RenamingElsewhereFor (fst env,c)) avoid na c else compute_displayed_name_in (RenamingElsewhereFor (fst env,c)) avoid na c in + let b = match decl with + | LocalAssum _ -> None + | LocalDef (_,b,_) -> Some b + in let b' = Option.map (detype (lax,false) avoid env sigma) b in let t' = detype (lax,false) avoid env sigma t in (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest |