Merge PR#402: Uniform attribute handling in interfaces

8 files changed, 13 insertions, 13 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 605914a01..9e0a2a03e 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -416,7 +416,7 @@ let qhyp_eq h1 h2 = match h1, h2 with
 | _ -> false
 
 let check_bindings bl =
-  match List.duplicates qhyp_eq (List.map pi2 bl) with
+  match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
     | NamedHyp s :: _ ->
 	user_err 
 	  (str "The variable " ++ pr_id s ++
@@ -512,7 +512,7 @@ let clenv_match_args bl clenv =
     let mvs = clenv_independent clenv in
     check_bindings bl;
     List.fold_left
-      (fun clenv (loc,b,c) ->
+      (fun clenv (loc,(b,c)) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
           if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
@@ -676,7 +676,7 @@ let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma ev in
   let ty = Retyping.get_type_of env sigma c in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+  let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
   let (ev, _) = destEvar sigma ev in
   let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
   sigma
@@ -711,7 +711,7 @@ let solve_evar_clause env sigma hyp_only clause = function
     error_not_right_number_missing_arguments len
 | ExplicitBindings lbind ->
   let () = check_bindings lbind in
-  let fold sigma (_, binder, c) =
+  let fold sigma (_, (binder, c)) =
     let ev = evar_of_binder clause.cl_holes binder in
     define_with_type sigma env ev c
   in
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8367c09b8..b9c925796 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -56,7 +56,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err ~loc 
+      user_err ?loc 
                 (str "Instance is not well-typed in the environment of " ++
                  Termops.pr_existential_key sigma evk ++ str ".")
   in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index fc8e635a0..5a717f166 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -68,7 +68,7 @@ module V82 = struct
 		Evd.evar_concl = concl;
 		Evd.evar_filter = Evd.Filter.identity;
 		Evd.evar_body = Evd.Evar_empty;
-		Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
+		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
 		Evd.evar_candidates = None;
 		Evd.evar_extra = extra }
     in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7622a8776..1bf65b8ae 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -130,7 +130,7 @@ val set_end_tac : Genarg.glob_generic_argument -> unit
 (** [set_used_variables l] declares that section variables [l] will be
     used in the proof *)
 val set_used_variables :
-  Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
 val get_used_variables : unit -> Context.Named.t option
 
 (** {6 Universe binders } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 01f883cde..2396db868 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -207,7 +207,7 @@ let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    CErrors.user_err ~loc
+    CErrors.user_err ?loc
       ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
@@ -287,13 +287,13 @@ let set_used_variables l =
     match entry with
     | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
-       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+       else (ctx, all_safe, (Loc.tag x)::to_clear) 
     | LocalDef (x,bo, ty) as decl ->
        if Id.Set.mem x all_safe then orig else
        let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
        if Id.Set.subset vars all_safe
        then (decl :: ctx, Id.Set.add x all_safe, to_clear)
-       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+       else (ctx, all_safe, (Loc.tag x) :: to_clear) in
   let ctx, _, to_clear =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
   let to_clear = if !proof_using_auto_clear then to_clear else [] in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e90fb5bc9..52bbd9ac5 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -140,7 +140,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+  Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
 val get_used_variables : unit -> Context.Named.t option
 
 val get_universe_binders : unit -> universe_binders option
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 2c489d6de..f0854e9aa 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -76,7 +76,7 @@ and full_set env =
   List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
-  let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+  let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in
   let v_ty = process_expr env ty_expr ty in
   let s = Id.Set.union v_ty (process_expr env e ty) in
   Id.Set.elements s
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1ee6e0ca5..d423a658a 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -137,7 +137,7 @@ let with_type env evd c t =
   let my_type = Retyping.get_type_of env evd c in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
-    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+    Coercion.inh_conv_coerce_to true env evd j t
   in
   evd , j'.Environ.uj_val