diff options
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 16 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 7 |
5 files changed, 18 insertions, 17 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 59feb46dc1..d4555707c4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -753,7 +753,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) + | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.fold mk_env terms Id.Map.empty in @@ -815,7 +815,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat + | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try diff --git a/interp/notation.ml b/interp/notation.ml index b9aca82cf4..56504db04e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1516,7 +1516,7 @@ let uninterp_prim_token c = with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - match glob_constr_of_closed_cases_pattern c with + match glob_constr_of_closed_cases_pattern (Global.env()) c with | exception Not_found -> raise Notation_ops.No_match | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7d7e10a05b..1f1cf4506f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1292,7 +1292,7 @@ let match_notation_constr u c (metas,pat) = | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> - let v = glob_constr_of_cases_pattern pat in + let v = glob_constr_of_cases_pattern (Global.env()) pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> @@ -1333,11 +1333,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in sigma,(0,l) | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in + let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 74432cc010..82e42d41be 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -539,8 +539,8 @@ let drop_local_defs params decls args = | _ -> assert false in aux decls args -let add_patterns_for_params_remove_local_defs (ind,j) l = - let (mib,mip) = Global.lookup_inductive ind in +let add_patterns_for_params_remove_local_defs env (ind,j) l = + let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.Declarations.mind_nparams in let l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then @@ -556,12 +556,12 @@ let add_alias ?loc na c = | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id)) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function +let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None)) | PatCstr (cstr,l,na) -> let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in - let l = add_patterns_for_params_remove_local_defs cstr l in - add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l)) + let l = add_patterns_for_params_remove_local_defs env cstr l in + add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux env isclosed) l)) | PatVar (Name id) when not isclosed -> GVar id | PatVar Anonymous when not isclosed -> @@ -571,14 +571,14 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo | _ -> raise Not_found ) x -let glob_constr_of_closed_cases_pattern p = match DAst.get p with +let glob_constr_of_closed_cases_pattern env p = match DAst.get p with | PatCstr (cstr,l,na) -> let loc = p.CAst.loc in - na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) + na,glob_constr_of_cases_pattern_aux env true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found -let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p +let glob_constr_of_cases_pattern env p = glob_constr_of_cases_pattern_aux env false p (* This has to be in some file... *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 2f0ac76235..47c65c2a72 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -96,12 +96,13 @@ val map_pattern : (glob_constr -> glob_constr) -> @raise Not_found if translation is impossible *) val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g -val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g +val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t * 'a glob_constr_g (** A canonical encoding of cases pattern into constr such that composed with [cases_pattern_of_glob_constr Anonymous] gives identity *) -val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g +val glob_constr_of_cases_pattern : Environ.env -> 'a cases_pattern_g -> 'a glob_constr_g -val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list +val add_patterns_for_params_remove_local_defs : Environ.env -> constructor -> + 'a cases_pattern_g list -> 'a cases_pattern_g list val empty_lvar : Ltac_pretype.ltac_var_map |