diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 19 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 21 |
3 files changed, 29 insertions, 13 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1d3b1bbb24..48fb4a4a5d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2530,12 +2530,12 @@ let intern_context env impl_env binders = binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) -let interp_glob_context_evars ?(program_mode=false) env sigma k bl = +let interp_glob_context_evars ?(program_mode=false) env sigma bl = let open EConstr in let flags = { Pretyping.all_no_fail_flags with program_mode } in - let env, sigma, par, _, impls = + let env, sigma, par, impls = List.fold_left - (fun (env,sigma,params,n,impls) (na, k, b, t) -> + (fun (env,sigma,params,impls) (na, k, b, t) -> let t' = if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t else t @@ -2551,16 +2551,17 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = | MaxImplicit -> CAst.make (Some (na,true)) :: impls | Explicit -> CAst.make None :: impls in - (push_rel d env, sigma, d::params, succ n, impls) + (push_rel d env, sigma, d::params, impls) | Some b -> let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in let r = Retyping.relevance_of_type env sigma t in let d = LocalDef (make_annot na r, c, t) in - (push_rel d env, sigma, d::params, n, impls)) - (env,sigma,[],k+1,[]) (List.rev bl) - in sigma, ((env, par), List.rev impls) + (push_rel d env, sigma, d::params, impls)) + (env,sigma,[],[]) (List.rev bl) + in + sigma, ((env, par), List.rev impls) -let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = +let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params = let int_env,bl = intern_context env impl_env params in - let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in + let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in sigma, (int_env, x) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2eb96aad56..898a3e09c8 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -156,7 +156,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * (** Interpret contexts: returns extended env and context *) val interp_context_evars : - ?program_mode:bool -> ?impl_env:internalization_env -> ?shift:int -> + ?program_mode:bool -> ?impl_env:internalization_env -> env -> evar_map -> local_binder_expr list -> evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) diff --git a/interp/notation.ml b/interp/notation.ml index 17ae045187..7e90e15b72 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1198,10 +1198,25 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function find_without_delimiters find (ntn_scope,ntn) scopes end | LonelyNotationItem ntn' :: scopes -> - begin match ntn_scope, ntn with - | LastLonelyNotation, Some ntn when notation_eq ntn ntn' -> - Some (None, None) + begin match ntn with + | Some ntn'' when notation_eq ntn' ntn'' -> + begin match ntn_scope with + | LastLonelyNotation -> + (* If the first notation with same string in the visibility stack + is the one we want to print, then it can be used without + risking a collision *) + Some (None, None) + | NotationInScope _ -> + (* A lonely notation is liable to hide the scoped notation + to print, we check if the lonely notation is active to + know if the delimiter of the scoped notationis needed *) + if find default_scope then + find_with_delimiters ntn_scope + else + find_without_delimiters find (ntn_scope,ntn) scopes + end | _ -> + (* A lonely notation which does not interfere with the notation to use *) find_without_delimiters find (ntn_scope,ntn) scopes end | [] -> |