diff options
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 02ee56ac5..0666ab4f1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -198,7 +198,7 @@ let rec alpha_pat excluded pat = | PatVar(Name id) -> if Id.List.mem id excluded then - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) else pat, excluded,Id.Map.empty @@ -206,7 +206,7 @@ let rec alpha_pat excluded pat = let new_na,new_excluded,map = match na with | Name id when Id.List.mem id excluded -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty | _ -> na,excluded,Id.Map.empty in @@ -261,7 +261,7 @@ let rec alpha_rt excluded rt = match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> - let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in + let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in @@ -276,7 +276,7 @@ let rec alpha_rt excluded rt = let new_c = alpha_rt excluded c in GLetIn(Anonymous,new_b,new_t,new_c) | GLambda(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let t,b = if Id.equal new_id id then t, b @@ -289,7 +289,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GLambda(Name new_id,k,new_t,new_b) | GProd(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let new_excluded = new_id::excluded in let t,b = if Id.equal new_id id @@ -302,7 +302,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GProd(Name new_id,k,new_t,new_b) | GLetIn(Name id,b,t,c) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let c = if Id.equal new_id id then c else change_vars (Id.Map.add id new_id Id.Map.empty) c @@ -320,7 +320,7 @@ let rec alpha_rt excluded rt = match na with | Anonymous -> (na::nal,excluded,mapping) | Name id -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in if Id.equal new_id id then na::nal,id::excluded,mapping @@ -741,7 +741,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -763,7 +763,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res |