From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- interp/implicit_quantifiers.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/implicit_quantifiers.mli') diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 71009ec3c2..945bed2aad 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -16,8 +16,8 @@ open Globnames val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> Loc.t * reference * constr_expr list * instance_expr option -val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list * instance_expr option +val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) located +val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation located option) list * instance_expr option) located (** Fragile, should be used only for construction a set of identifiers to avoid *) @@ -31,7 +31,7 @@ val free_vars_of_binders : order with the location of their first occurrence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> - glob_constr -> (Id.t * Loc.t) list + glob_constr -> Id.t located list val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t -- cgit v1.2.3