[constrexpr] Make patterns use Loc.located for location information

This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.

Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.

Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.

`git grep 'Loc.t \*'` gives an overview of the remaining work to do.

We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.

1 files changed, 12 insertions, 5 deletions

diff --git a/lib/loc.mli b/lib/loc.mli
index bb88f8642..fef1d8938 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -18,9 +18,6 @@ type t = {
   ep : int; (** end position *)
 }
 
-type 'a located = t * 'a
-(** Embed a location in a type *)
-
 (** {5 Location manipulation} *)
 
 (** This is inherited from CAMPL4/5. *)
@@ -54,12 +51,22 @@ val get_loc : Exninfo.info -> t option
 val raise : ?loc:t -> exn -> 'a
 (** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *)
 
-(** {5 Location utilities} *)
+(** {5 Objects with location information } *)
+
+type 'a located = t * 'a
+(** Embed a location in a type *)
+
+(** Warning, this API is experimental  *)
+
+val to_pair : 'a located -> t * 'a
+val tag : ?loc:t -> 'a -> 'a located
 
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val down_located : ('a -> 'b) -> 'a located -> 'b
+
+(* Current not used *)
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 
-val down_located : ('a -> 'b) -> 'a located -> 'b
 (** Projects out a located object *)
 
 (** {5 Backward compatibility} *)