diff options
| -rw-r--r-- | interp/constrextern.ml | 15 | ||||
| -rw-r--r-- | interp/constrintern.ml | 28 | ||||
| -rw-r--r-- | interp/notation.ml | 8 | ||||
| -rw-r--r-- | interp/topconstr.ml | 4 | ||||
| -rw-r--r-- | interp/topconstr.mli | 4 |
5 files changed, 15 insertions, 44 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8c81e066ad..600392811b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -360,9 +360,6 @@ let make_pat_notation loc ntn l = (fun (loc,p) -> CPatPrim (loc,p)) destPatPrim l -let find_arguments_scope ref = - List.map (option_map (fun sc -> LightTmpScope sc)) (find_arguments_scope ref) - let bind_env sigma var v = try let vvar = List.assoc var sigma in @@ -445,9 +442,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = - if (* recursive *) false then option_cons scopt scopes - else scopes in + let scopes' = option_cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,scl@scopes') vars c) @@ -755,7 +750,7 @@ let rec extern inctx scopes vars r = | RDynamic (loc,d) -> CDynamic (loc,d) and extern_typ (_,scopes) = - extern true (Some (LightTmpScope (Notation.type_scope)),scopes) + extern true (Some Notation.type_scope,scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) @@ -823,9 +818,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = - if (* recursive *) false then option_cons scopt scopes - else scopes in + let scopes' = option_cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true @@ -866,7 +859,7 @@ let extern_constr_gen at_top scopt env t = extern (not at_top) (scopt,[]) vars r let extern_constr_in_scope at_top scope env t = - extern_constr_gen at_top (Some (ExplicitTmpScope scope)) env t + extern_constr_gen at_top (Some scope) env t let extern_constr at_top env t = extern_constr_gen at_top None env t diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 95fcf0d9a8..386f1f4a20 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -221,18 +221,7 @@ let contract_pat_notation ntn l = (**********************************************************************) (* Remembering the parsing scope of variables in notations *) -let make_light_tmp_scope = function - | Some sc -> Some (LightTmpScope sc) - | None -> None - -let make_current_scope (tmp_scope,scopes) = - let scopes = if (* recursive *) false then scopes else [] in - match tmp_scope with - | Some (ExplicitTmpScope sc) -> sc :: scopes - | _ -> scopes - -let find_arguments_scope ref = - List.map make_light_tmp_scope (find_arguments_scope ref) +let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes let set_var_scope loc id (_,scopt,scopes) varscopes = let idscopes = List.assoc id varscopes in @@ -242,7 +231,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes = user_err_loc (loc,"set_var_scope", pr_id id ++ str " already occurs in a different scope") else - idscopes := Some (scopt,if (* recursive *) false then scopes else []) + idscopes := Some (scopt,scopes) (**********************************************************************) (* Discriminating between bound variables and global references *) @@ -258,7 +247,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id = let l,impl,argsc = List.assoc id impls in let l = List.map (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in - RVar (loc,id), impl, List.map make_light_tmp_scope argsc, l + RVar (loc,id), impl, argsc, l with Not_found -> (* Is [id] bound in current env or is an ltac var bound to constr *) if Idset.mem id env or List.mem id vars1 @@ -581,8 +570,8 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = if !dump then dump_notation_location (fst (unloc loc)) df; (ids,[subst,c]) | CPatDelimiters (loc, key, e) -> - intern_cases_pattern genv scopes aliases - (Some (ExplicitTmpScope (find_delimiters_scope loc key))) e + intern_cases_pattern genv (find_delimiters_scope loc key::scopes) + aliases None e | CPatAtom (loc, Some head) -> (match maybe_constructor head with | ConstrPat (c,args) -> @@ -763,7 +752,7 @@ let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = subst_aconstr_in_rawconstr loc intern subst env c let set_type_scope (ids,tmp_scope,scopes) = - (ids,Some (LightTmpScope Notation.type_scope),scopes) + (ids,Some Notation.type_scope,scopes) let reset_tmp_scope (ids,tmp_scope,scopes) = (ids,None,scopes) @@ -862,8 +851,7 @@ let internalise sigma globalenv env allow_soapp lvar c = if !dump then dump_notation_location (fst (unloc loc)) df; c | CDelimiters (loc, key, e) -> - let tmp_scope = ExplicitTmpScope (find_delimiters_scope loc key) in - intern (ids,Some tmp_scope,scopes) e + intern (ids,None,find_delimiters_scope loc key::scopes) e | CAppExpl (loc, (isproj,ref), args) -> let (f,_,args_scopes,_) = intern_reference env lvar ref in check_projection isproj (List.length args) f; @@ -1077,7 +1065,7 @@ let intern_gen isarity sigma env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let tmp_scope = - if isarity then Some (LightTmpScope Notation.type_scope) else None in + if isarity then Some Notation.type_scope else None in internalise sigma env (extract_ids env, tmp_scope,[]) allow_soapp (ltacvars,Environ.named_context env, [], impls) c diff --git a/interp/notation.ml b/interp/notation.ml index 0e6f02c52c..c218e5cf3f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -133,13 +133,7 @@ let push_scopes = List.fold_right push_scope type local_scopes = tmp_scope_name option * scope_name list let make_current_scopes (tmp_scope,scopes) = - match tmp_scope with - | Some (ExplicitTmpScope sc) -> - if (* recursive *) false - then push_scope sc (push_scopes scopes !scope_stack) - else [Scope sc] - | Some (LightTmpScope sc) -> push_scope sc (push_scopes scopes !scope_stack) - | None -> push_scopes scopes !scope_stack + option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) (**********************************************************************) (* Delimiters *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c9ae593afd..213b9a48e9 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -480,9 +480,7 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (_,patl2,rhs2) = type scope_name = string -type tmp_scope_name = - | LightTmpScope of scope_name - | ExplicitTmpScope of scope_name +type tmp_scope_name = scope_name type interpretation = (identifier * (tmp_scope_name option * scope_name list)) list * aconstr diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 0d428e8fa3..85514c1395 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -61,9 +61,7 @@ exception No_match type scope_name = string -type tmp_scope_name = - | LightTmpScope of scope_name - | ExplicitTmpScope of scope_name +type tmp_scope_name = scope_name type interpretation = (identifier * (tmp_scope_name option * scope_name list)) list * aconstr |