[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.

2 files changed, 7 insertions, 7 deletions

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a6a6bd6f9..0bc3f502c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -63,7 +63,7 @@ DECLARE PLUGIN "ssrmatching_plugin"
 
 type loc = Loc.t
 let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
-let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
+let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg)
 let ppnl = Feedback.msg_info
 
 (* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
@@ -1071,7 +1071,7 @@ GEXTEND Gram
   GLOBAL: cpattern;
   cpattern: [[ k = ssrtermkind; c = constr ->
     let pattern = mk_term k c in
-    if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]];
+    if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]];
 END
 
 ARGUMENT EXTEND lcpattern
@@ -1088,7 +1088,7 @@ GEXTEND Gram
   GLOBAL: lcpattern;
   lcpattern: [[ k = ssrtermkind; c = lconstr ->
     let pattern = mk_term k c in
-    if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]];
+    if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]];
 END
 
 let thin id sigma goal =
@@ -1187,16 +1187,16 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red));
   let red = match redty with None -> red | Some ty -> let ty = ' ', ty in
   match red with
-  | T t -> T (combineCG t ty (mkCCast ~loc:(loc_ofCG t)) mkRCast)
+  | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
   | X_In_T (x,t) ->
       let ty = pf_intern_term ist gl ty in
       E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t)
   | E_In_X_In_T (e,x,t) ->
       let ty = mkG (pf_intern_term ist gl ty) in
-      E_In_X_In_T (combineCG e ty (mkCCast ~loc:(loc_ofCG t)) mkRCast, x, t)
+      E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | E_As_X_In_T (e,x,t) ->
       let ty = mkG (pf_intern_term ist gl ty) in
-      E_As_X_In_T (combineCG e ty (mkCCast ~loc:(loc_ofCG t)) mkRCast, x, t)
+      E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | red -> red in
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn ?loc x (a,(g,c)) = match c with
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 894cdb943..a8862d264 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -222,7 +222,7 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
 val tag_of_cpattern : cpattern -> char
-val loc_of_cpattern : cpattern -> Loc.t
+val loc_of_cpattern : cpattern -> Loc.t option
 val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern