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.
---
 engine/evarutil.mli | 12 ++++++------
 engine/evd.ml       |  6 +++---
 engine/uState.ml    |  2 +-
 3 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ca9591e71b..fcc435a2ec 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -22,13 +22,13 @@ val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> types -> (constr, 'r) Sigma.sigma
 
 val new_pure_evar :
-  named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  named_context_val -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> types -> (evar, 'r) Sigma.sigma
@@ -37,7 +37,7 @@ val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
 
 (** the same with side-effects *)
 val e_new_evar :
-  env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> types -> constr
@@ -45,12 +45,12 @@ val e_new_evar :
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
   (constr * sorts, 'r) Sigma.sigma
 
 val e_new_type_evar : env -> evar_map ref ->
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
 val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
@@ -72,7 +72,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    as a telescope) is [sign] *)
 val new_evar_instance :
  named_context_val -> 'r Sigma.t -> types -> 
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
+  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
   constr list -> (constr, 'r) Sigma.sigma
diff --git a/engine/evd.ml b/engine/evd.ml
index 9e81ccd360..b0531d5814 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -704,10 +704,10 @@ let extract_all_conv_pbs evd =
 
 let loc_of_conv_pb evd (pbty,env,t1,t2) =
   match kind_of_term (fst (decompose_app t1)) with
-  | Evar (evk1,_) -> Some (fst (evar_source evk1 evd))
+  | Evar (evk1,_) -> fst (evar_source evk1 evd)
   | _ ->
   match kind_of_term (fst (decompose_app t2)) with
-  | Evar (evk2,_) -> Some (fst (evar_source evk2 evd))
+  | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
 (** The following functions return the set of evars immediately
@@ -794,7 +794,7 @@ let make_evar_universe_context e l =
   | Some us ->
       List.fold_left
         (fun uctx (loc,id) ->
-        fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx))
+        fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx))
         uctx us
 
 (****************************************)
diff --git a/engine/uState.ml b/engine/uState.ml
index c9653b6cdf..eb1acb8450 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -255,7 +255,7 @@ let universe_context ?names ctx =
           let l =
             try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
             with Not_found ->
-              user_err ~loc ~hdr:"universe_context"
+              user_err ?loc ~hdr:"universe_context"
                             (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
           in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
          pl ([], [], levels)
-- 
cgit v1.2.3