diff options
| -rw-r--r-- | dev/doc/changes.md | 5 | ||||
| -rw-r--r-- | interp/constrextern.ml | 7 | ||||
| -rw-r--r-- | interp/constrintern.ml | 20 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 10 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 2 |
5 files changed, 25 insertions, 19 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 5adeafaa38..26c4b01c9f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -37,6 +37,11 @@ Dumpglob: plugins to temporarily change/pause the output of Dumpglob, and then restore it to the original setting. +Glob_term: + +- Removing useless `binding_kind` argument of `GLocalDef` in + `extended_glob_local_binder`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3969c7ea1f..f3ba884856 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -886,9 +886,10 @@ let extern_prim_token_delimiter_if_required n key_n scope_n scopes = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> + assert (bk = Explicit); match DAst.get t with - | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) - | _ -> GLocalDef (p,bk,x,Some t) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,x,None) + | _ -> GLocalDef (p,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -1217,7 +1218,7 @@ and extern_local_binder scopes vars = function [] -> ([],[],[]) | b :: l -> match DAst.get b with - | GLocalDef (na,bk,bd,ty) -> + | GLocalDef (na,bd,ty) -> let (assums,ids,l) = extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in (assums,na::ids, diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e3a4d1b169..70a4ea35e9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -560,10 +560,10 @@ let intern_assumption intern ntnvars env nal bk ty = let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) - | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) - | GLocalDef (na,bk,c,None) -> + | GLocalDef (na,c,Some t) -> (na,Explicit,Some c,t) + | GLocalDef (na,c,None) -> let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in - (na,bk,Some c,t) + (na,Explicit,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ) @@ -575,7 +575,7 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in (push_name_env ntnvars impls env locna, - (na,Explicit,term,ty)) + (na,term,ty)) let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) = let p,t = match p with @@ -606,8 +606,8 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef( {loc; v=na} as locna,def,ty) -> - let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in - env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl + let env,(na,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in + env, (DAst.make ?loc @@ GLocalDef (na,def,ty)) :: bl | CLocalPattern p -> let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl) @@ -650,7 +650,7 @@ let rec expand_binders ?loc mk bl c = | [] -> c | b :: bl -> match DAst.get b with - | GLocalDef (n, bk, b, oty) -> + | GLocalDef (n, b, oty) -> expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c)) | GLocalAssum (n, bk, t) -> expand_binders ?loc mk bl (mk ?loc (n,bk,t) c) @@ -794,8 +794,8 @@ let terms_of_binders bl = let loc = bnd.loc in begin match DAst.get bnd with | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l - | GLocalDef (Name id,_,_,_) -> extract_variables l - | GLocalDef (Anonymous,_,_,_) + | GLocalDef (Name id,_,_) -> extract_variables l + | GLocalDef (Anonymous,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l | GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc () @@ -847,7 +847,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | AddTermIter nterms::rest,terminator,iter -> aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter | AddLetIn (na,c,t)::rest,terminator,iter -> - let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in + let env,(na,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 036970ce37..0e7f085bde 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -863,7 +863,7 @@ let rec push_context_binders vars = function let vars = match DAst.get b with | GLocalAssum (na,_,_) -> Termops.add_vname vars na | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars - | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in + | GLocalDef (na,_,_) -> Termops.add_vname vars na in push_context_binders vars bl let is_term_meta id metas = @@ -1014,9 +1014,9 @@ let unify_binder_upto alp b b' = | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> let alp, na = unify_name_upto alp na na' in alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') - | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> + | GLocalDef (na,c,t), GLocalDef (na',c',t') -> let alp, na = unify_name_upto alp na na' in - alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + alp, DAst.make ?loc @@ GLocalDef (na, unify_term alp c c', unify_opt_term alp t t') | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' -> let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') @@ -1061,7 +1061,7 @@ let rec unify_terms_binders alp cl bl' = | [], [] -> [] | c :: cl, b' :: bl' -> begin match DAst.get b' with - | GLocalDef ( _, _, _, t) -> unify_terms_binders alp cl bl' + | GLocalDef (_, _, t) -> unify_terms_binders alp cl bl' | _ -> unify_term_binder alp c b' :: unify_terms_binders alp cl bl' end | _ -> raise No_match @@ -1249,7 +1249,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = with No_match -> match DAst.get rest with | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls -> - let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in + let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,c,t) in (* collect let-in *) (try aux true sigma (b::bl) rest' with OnlyTrailingLetIns diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a957bc0fcd..9f93e5e6c1 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -137,7 +137,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g - | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option + | GLocalDef of Name.t * 'a glob_constr_g * 'a glob_constr_g option | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t |