From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Jan 2017 01:27:40 +0100
Subject: [location] Use Loc.located for constr_expr.

This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.

Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
---
 interp/constrexpr_ops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrexpr_ops.mli')

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index f6d97e107d..ae5ec2be5c 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -49,10 +49,10 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
 val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
-val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCLambdaN : loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [abstract_constr_expr], with location *)
 
-val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCProdN : loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
 (** @deprecated variant of mkCLambdaN *)
-- 
cgit v1.2.3


From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 interp/constrexpr_ops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/constrexpr_ops.mli')

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index ae5ec2be5c..82e4f54b08 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
 val constr_loc : constr_expr -> Loc.t
 val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
 val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
-val local_binders_loc : local_binder_expr list -> Loc.t
+val local_binders_loc : local_binder_expr list -> Loc.t option
 
 (** {6 Constructors}*)
 
@@ -49,10 +49,10 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
 val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
-val mkCLambdaN : loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [abstract_constr_expr], with location *)
 
-val mkCProdN : loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
 (** @deprecated variant of mkCLambdaN *)
-- 
cgit v1.2.3


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 <unknown> 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 <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
---
 interp/constrexpr_ops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/constrexpr_ops.mli')

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 82e4f54b08..d51576c04d 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -34,9 +34,9 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
 
 (** {6 Retrieving locations} *)
 
-val constr_loc : constr_expr -> Loc.t
-val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
+val constr_loc : constr_expr -> Loc.t option
+val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
+val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t option
 val local_binders_loc : local_binder_expr list -> Loc.t option
 
 (** {6 Constructors}*)
-- 
cgit v1.2.3