Merge PR#402: Uniform attribute handling in interfaces

6 files changed, 18 insertions, 18 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e85c1f6fd8..6cba6f6075 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -365,7 +365,7 @@ let push_rel_context_to_named_context env sigma typ =
  * Entry points to define new evars   *
  *------------------------------------*)
 
-let default_source = (Loc.ghost,Evar_kinds.InternalHole)
+let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
 let restrict_evar evd evk filter candidates =
   let evd = Sigma.to_evar_map evd in
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 db048bbd6e..8ade6cb996 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -149,7 +149,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
-  evar_source = (Loc.ghost,Evar_kinds.InternalHole);
+  evar_source = Loc.tag @@ Evar_kinds.InternalHole;
   evar_candidates = None;
   evar_extra = Store.empty
 }
@@ -704,7 +704,7 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
   | _ ->
   match kind_of_term (fst (decompose_app t2)) with
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
-  | _ -> Loc.ghost
+  | _             -> None
 
 (** The following functions return the set of evars immediately
     contained in the object *)
@@ -790,7 +790,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
 
 (****************************************)
@@ -1082,8 +1082,8 @@ let retract_coercible_metas evd =
 
 let evar_source_of_meta mv evd =
   match meta_name evd mv with
-  | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
-  | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
+  | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+  | Name id   -> Loc.tag @@ Evar_kinds.VarInstance id
 
 let dependent_evar_ident ev evd =
   let evi = find evd ev in
diff --git a/engine/evd.mli b/engine/evd.mli
index 9c40c8b715..0053324706 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -414,7 +414,7 @@ val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
+val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 
 (** The following functions return the set of evars immediately
     contained in the object; need the term to be evar-normal otherwise
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 99bd4bc4ff..7f80d40d64 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -66,7 +66,7 @@ let dependent_init =
      for type classes. *)
   let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
   (* Goals don't have a source location. *)
-  let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+  let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
diff --git a/engine/uState.ml b/engine/uState.ml
index e27d0536d6..dc68220575 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -258,7 +258,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)
@@ -269,10 +269,10 @@ let universe_context ?names ctx =
            try
              let info =
                Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
-             Option.default Loc.ghost info.uloc
-           with Not_found -> Loc.ghost
+             info.uloc
+           with Not_found -> None
          in
-           user_err ~loc ~hdr:"universe_context"
+           user_err ?loc ~hdr:"universe_context"
                         ((str(CString.plural n "Universe") ++ spc () ++
 			     Univ.LSet.pr (pr_uctx_level ctx) left ++
 			   spc () ++ str (CString.conjugate_verb_to_be n) ++