diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a96deca06..af8cc43c1 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -74,7 +74,7 @@ module PrintingInductiveMake = let kn' = subst_ind subst kn in if kn' == kn then obj else kn', ints - let printer ind = pr_global_env Idset.empty (IndRef ind) + let printer ind = pr_global_env Id.Set.empty (IndRef ind) let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) @@ -175,11 +175,11 @@ let lookup_name_as_displayed env t s = let rec lookup avoid n c = match kind_of_term c with | Prod (name,_,c') -> (match compute_displayed_name_in RenamingForGoal avoid name c' with - | (Name id,avoid') -> if id_eq id s then Some n else lookup avoid' (n+1) c' + | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> (match compute_displayed_name_in RenamingForGoal avoid name c' with - | (Name id,avoid') -> if id_eq id s then Some n else lookup avoid' (n+1) c' + | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None @@ -231,7 +231,7 @@ let rec decomp_branch n nal b (avoid,env as e) c = | Lambda (na,_,c) -> na,c,compute_displayed_let_name_in | LetIn (na,_,_,c) -> na,c,compute_displayed_name_in | _ -> - Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])), + Name (Id.of_string "x"),(applist (lift 1 c, [mkRel 1])), compute_displayed_name_in in let na',avoid' = f flag avoid na c in decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c @@ -293,7 +293,7 @@ let it_destRLambda_or_LetIn_names n c = | _ -> (* eta-expansion *) let next l = - let x = next_ident_away (id_of_string "x") l in + let x = next_ident_away (Id.of_string "x") l in (* Not efficient but unusual and no function to get free glob_vars *) (* if occur_glob_constr x c then next (x::l) else x in *) x @@ -386,7 +386,7 @@ let rec detype (isgoal:bool) avoid env t = | Anonymous -> !detype_anonymous dl n with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (dl, id_of_string s)) + in GVar (dl, Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) GEvar (dl, n, None) |