From 4d25b224b91959b85fcd68c825a307ec684f0bac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 28 Feb 2016 18:28:14 +0100 Subject: Printing notations: Cleaning in anticipation of fixing #4592. - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env. --- interp/constrintern.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrintern.mli') diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 73ecc437d..eea76aa31 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -185,7 +185,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr guaranteed to have the same domain as the input one. *) val interp_notation_constr : ?impls:internalization_env -> notation_interp_env -> constr_expr -> - (subscopes * notation_var_internalization_type) Id.Map.t * + (bool * subscopes * notation_var_internalization_type) Id.Map.t * notation_constr (** Globalization options *) -- cgit v1.2.3