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

10 files changed, 96 insertions, 95 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f5e2e52a1..eb0d01718 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -349,15 +349,15 @@ let find_tomatch_tycon evdref env loc = function
 
 let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let loc = loc_of_glob_constr tomatch in
-  let tycon,realnames = find_tomatch_tycon evdref env (Some loc) indopt in
+  let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
   let j = typing_fun tycon env evdref tomatch in
-  let evd, j = Coercion.inh_coerce_to_base ~loc:(loc_of_glob_constr tomatch) env !evdref j in
+  let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
   let typ = nf_evar !evdref j.uj_type in
   let t =
     try try_find_ind env !evdref typ realnames
     with Not_found ->
-      unify_tomatch_with_patterns evdref env (Some loc) typ pats realnames in
+      unify_tomatch_with_patterns evdref env loc typ pats realnames in
   (j.uj_val,t)
 
 let coerce_to_indtype typing_fun evdref env matx tomatchl = 
@@ -427,7 +427,7 @@ let current_pattern eqn =
     | pat::_ -> pat
     | [] -> anomaly (Pp.str "Empty list of patterns")
 
-let alias_of_pat = Loc.with_loc (fun ~loc -> function
+let alias_of_pat = Loc.with_loc (fun ?loc -> function
   | PatVar name -> name
   | PatCstr(_,_,name) -> name
   )
@@ -489,23 +489,23 @@ let check_and_adjust_constructor env ind cstrs = function
 	if Int.equal (List.length args) nb_args_constr then pat
 	else
 	  try
-	    let args' = adjust_local_defs ~loc (args, List.rev ci.cs_args)
-	    in Loc.tag ~loc @@ PatCstr (cstr, args', alias)
+	    let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
+	    in Loc.tag ?loc @@ PatCstr (cstr, args', alias)
 	  with NotAdjustable ->
-	    error_wrong_numarg_constructor ~loc env cstr nb_args_constr
+	    error_wrong_numarg_constructor ?loc env cstr nb_args_constr
       else
 	(* Try to insert a coercion *)
 	try
-	  Coercion.inh_pattern_coerce_to ~loc env pat ind' ind
+	  Coercion.inh_pattern_coerce_to ?loc env pat ind' ind
 	with Not_found ->
-	  error_bad_constructor ~loc env cstr ind
+	  error_bad_constructor ?loc env cstr ind
 
 let check_all_variables env sigma typ mat =
   List.iter
     (fun eqn -> match current_pattern eqn with
        | _,   PatVar id -> ()
        | loc, PatCstr (cstr_sp,_,_) ->
-	   error_bad_pattern ~loc env sigma cstr_sp typ)
+	   error_bad_pattern ?loc env sigma cstr_sp typ)
     mat
 
 let check_unused_pattern env eqn =
@@ -1545,7 +1545,7 @@ let matx_of_eqns env eqns =
 	it = Some initial_rhs } in
     { patterns = initial_lpat;
       alias_stack = [];
-      eqn_loc = Some loc;
+      eqn_loc = loc;
       used = ref false;
       rhs = rhs }
   in List.map build_eqn eqns
@@ -1853,7 +1853,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		       | None -> [LocalAssum (na, lift n typ)]
 		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
 	    | Some (loc,_) ->
- 	    user_err ~loc 
+ 	    user_err ?loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
@@ -1865,7 +1865,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	    match t with
 	      | Some (loc,(ind',realnal)) ->
 		  if not (eq_ind ind ind') then
-		    user_err ~loc  (str "Wrong inductive type.");
+		    user_err ?loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
 		  List.rev realnal
@@ -2073,7 +2073,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
 		Name id, id :: avoid
 	in
-	  ((Loc.tag ~loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
+	  ((Loc.tag ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
     | PatCstr (((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
@@ -2084,7 +2084,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	in
 	let (ind,u), params = dest_ind_family indf in
 	let params = List.map EConstr.of_constr params in
-	if not (eq_ind ind cind) then error_bad_constructor ~loc env cstr ind;
+	if not (eq_ind ind cind) then error_bad_constructor ?loc env cstr ind;
 	let cstrs = get_constructors env indf in
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
@@ -2104,7 +2104,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	in
 	let args = List.rev args in
 	let patargs = List.rev patargs in
-	let pat' = Loc.tag ~loc @@ PatCstr (cstr, patargs, alias) in
+	let pat' = Loc.tag ?loc @@ PatCstr (cstr, patargs, alias) in
 	let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in
 	let app = applist (cstr, List.map (lift (List.length sign)) params) in
 	let app = applist (app, args) in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 3079d1052..721d1d749 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -68,14 +68,14 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 let encode_bool r =
   let (x,lc) = encode_inductive r in
   if not (has_two_constructors lc) then
-    user_err ~loc:(loc_of_reference r) ~hdr:"encode_if"
+    user_err ?loc:(loc_of_reference r) ~hdr:"encode_if"
       (str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
   let (x,lc) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
-    user_err ~loc:(loc_of_reference r) ~hdr:"encode_tuple"
+    user_err ?loc:(loc_of_reference r) ~hdr:"encode_tuple"
       (str "This type cannot be seen as a tuple type.");
   x
 
@@ -793,7 +793,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)
 
-let rec subst_cases_pattern subst (loc, pat) = Loc.tag ~loc @@
+let rec subst_cases_pattern subst (loc, pat) = Loc.tag ?loc @@
   match pat with
   | PatVar _ -> pat
   | PatCstr (((kn,i),j),cpl,n) ->
@@ -804,7 +804,7 @@ let rec subst_cases_pattern subst (loc, pat) = Loc.tag ~loc @@
 
 let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
-let rec subst_glob_constr subst (loc, raw) = Loc.tag ~loc @@
+let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@
   match raw with
   | GRef (ref,u) ->
       let ref',t = subst_global subst ref in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 95680e18a..1318942c5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1268,7 +1268,7 @@ let solve_unconstrained_impossible_cases env evd =
     match ev_info.evar_source with
     | loc,Evar_kinds.ImpossibleCase ->
       let j, ctx = coq_unit_judge () in
-      let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
+      let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
       let ty = j_type j in
       let conv_algo = evar_conv_x full_transparent_state in
       let evd' = check_evar_instance evd' evk ty conv_algo in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index c5ae684e3..c2b267dd8 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -181,7 +181,7 @@ let define_evar_as_sort env evd (ev,args) =
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
-let split_tycon loc env evd tycon =
+let split_tycon ?loc env evd tycon =
   let rec real_split evd c =
     let t = Reductionops.whd_all env evd c in
       match EConstr.kind evd t with
@@ -193,7 +193,7 @@ let split_tycon loc env evd tycon =
 	| App (c,args) when isEvar evd c ->
 	    let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in
 	    real_split evd' (mkApp (lam,args))
-	| _ -> error_not_product ~loc env evd c
+	| _ -> error_not_product ?loc env evd c
   in
     match tycon with
       | None -> evd,(Anonymous,None,None)
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index 2f7ac4efb..b8134a28c 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -31,7 +31,7 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
   evar_map * existential
 
 val split_tycon :
-  Loc.t -> env ->  evar_map -> type_constraint ->
+  ?loc:Loc.t -> env ->  evar_map -> type_constraint ->
     evar_map * (Name.t * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index cba1780ba..7e6b063d0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -354,7 +354,7 @@ let add_and_check_ident id set =
   Id.Set.add id set
 
 let bound_glob_vars =
-  let rec vars bound = Loc.with_loc (fun ~loc -> function
+  let rec vars bound = Loc.with_loc (fun ?loc -> function
     | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) as c ->
         let bound = name_fold add_and_check_ident na bound in
         fold_glob_constr vars bound (loc, c)
@@ -495,7 +495,7 @@ let rename_var l id =
     if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
     else id
 
-let rec rename_glob_vars l = Loc.map_with_loc (fun ~loc -> function
+let rec rename_glob_vars l = Loc.map_with_loc (fun ?loc -> function
   | GVar id as r ->
       let id' = rename_var l id in
       if id == id' then r else GVar id'
@@ -558,10 +558,10 @@ let rec cases_pattern_of_glob_constr na = Loc.map (function
   )
 
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ~loc -> function
+let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ?loc -> function
   | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
   | PatCstr (cstr,l,Anonymous)  ->
-      let ref = Loc.tag ~loc @@ GRef (ConstructRef cstr,None) in
+      let ref = Loc.tag ?loc @@ GRef (ConstructRef cstr,None) in
       GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
   ) x
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index ac2118ba7..dae662747 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -20,7 +20,7 @@ val glob_constr_eq : glob_constr -> glob_constr -> bool
 
 (** Operations on [glob_constr] *)
 
-val cases_pattern_loc : cases_pattern -> Loc.t
+val cases_pattern_loc : cases_pattern -> Loc.t option
 
 val cases_predicate_names : tomatch_tuples -> Name.t list
 
@@ -41,7 +41,8 @@ val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
 val bound_glob_vars : glob_constr -> Id.Set.t
-val loc_of_glob_constr : glob_constr -> Loc.t
+(* Obsolete *)
+val loc_of_glob_constr : glob_constr -> Loc.t option
 val glob_visible_short_qualid : glob_constr -> Id.t list
 
 (* Renaming free variables using a renaming map; fails with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 6696e174b..84d846afd 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,7 +324,7 @@ let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
     (fun () -> Pp.strbrk "Casts are ignored in patterns")
 
-let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
+let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
   | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
@@ -362,7 +362,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda c na = Loc.tag ~loc @@
+      let mkGLambda c na = Loc.tag ?loc @@
 	GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
@@ -391,7 +391,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
         | (None | Some (_, GHole _)), _ -> PMeta None
 	| Some p, None ->
-            user_err ~loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
+            user_err ?loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
@@ -404,7 +404,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r -> err ~loc (Pp.str "Non supported pattern.")
+  | r -> err ?loc (Pp.str "Non supported pattern.")
   )
 
 and pats_of_glob_branches loc metas vars ind brs =
@@ -412,7 +412,7 @@ and pats_of_glob_branches loc metas vars ind brs =
     | _, PatVar na ->
       name_iter (fun n -> metas := n::!metas) na;
       na
-    | loc, PatCstr(_,_,_) -> err ~loc (Pp.str "Non supported pattern.")
+    | loc, PatCstr(_,_,_) -> err ?loc (Pp.str "Non supported pattern.")
   in
   let rec get_pat indexes = function
     | [] -> false, []
@@ -421,10 +421,10 @@ and pats_of_glob_branches loc metas vars ind brs =
       let () = match ind with
       | Some sp when eq_ind sp indsp -> ()
       | _ ->
-        err ~loc (Pp.str "All constructors must be in the same inductive type.")
+        err ?loc (Pp.str "All constructors must be in the same inductive type.")
       in
       if Int.Set.mem (j-1) indexes then
-	err ~loc
+	err ?loc
           (str "No unique branch for " ++ int j ++ str"-th constructor.");
       let lna = List.map get_arg lv in
       let vars' = List.rev lna @ vars in
@@ -432,7 +432,7 @@ and pats_of_glob_branches loc metas vars ind brs =
       let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
       let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
       ext, ((j-1, tags, pat) :: pats)
-    | (loc,(_,_,_)) :: _ -> err ~loc (Pp.str "Non supported pattern.")
+    | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 24f6d1689..ef187e7a6 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -177,7 +177,7 @@ let unsatisfiable_constraints env evd ev comp =
   | Some ev ->
     let loc, kind = Evd.evar_source ev evd in
     let err = UnsatisfiableConstraints (Some (ev, kind), comp) in
-    Loc.raise ~loc (PretypeError (env,evd,err))
+    Loc.raise ?loc (PretypeError (env,evd,err))
 
 let unsatisfiable_exception exn =
   match exn with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fe15cb490..a256eaa5d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -216,8 +216,8 @@ let interp_universe_level_name evd (loc,s) =
           evd, snd (Idmap.find id names)
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
-  	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-	  else user_err ~loc ~hdr:"interp_universe_level_name"
+  	    new_univ_level_variable ?loc ~name:s univ_rigid evd
+	  else user_err ?loc ~hdr:"interp_universe_level_name"
 			     (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
@@ -229,8 +229,8 @@ let interp_universe ?loc evd = function
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
-let interp_level_info loc evd : Misctypes.level_info -> _ = function
-  | None -> new_univ_level_variable ~loc univ_rigid evd
+let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
+  | None -> new_univ_level_variable ?loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name evd (loc,s)
 
 let interp_sort ?loc evd = function
@@ -337,7 +337,7 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 	match k with
 	| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
 	| _ ->
-	    error_unsolvable_implicit ~loc env current_sigma evk None) pending
+	    error_unsolvable_implicit ?loc env current_sigma evk None) pending
 
 (* [check_evars] fails if some unresolved evar remains *)
 
@@ -349,7 +349,7 @@ let check_evars env initial_sigma sigma c =
         let (loc,k) = evar_source evk sigma in
         begin match k with
           | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
-          | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None
+          | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
         end
     | _ -> EConstr.iter sigma proc_rec c
   in proc_rec c
@@ -393,9 +393,9 @@ let check_instance loc subst = function
   | [] -> ()
   | (id,_) :: _ ->
       if List.mem_assoc id subst then
-        user_err ~loc  (pr_id id ++ str "appears more than once.")
+        user_err ?loc  (pr_id id ++ str "appears more than once.")
       else
-        user_err ~loc  (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+        user_err ?loc  (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
 
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
@@ -475,7 +475,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
 	(* and build a nice error message *)
       if Id.Map.mem id lvar.ltac_genargs then begin
         let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
-	user_err ~loc 
+	user_err ?loc 
          (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
           bound to a " ++ Geninterp.Val.pr typ ++ str ".")
       end;
@@ -484,47 +484,47 @@ let pretype_id pretype k0 loc env evdref lvar id =
 	  { uj_val  = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
       with Not_found ->
 	  (* [id] not found, standard error message *)
-	  error_var_not_found ~loc id
+	  error_var_not_found ?loc id
 
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_glob_level loc evd : Misctypes.glob_level -> _ = function
+let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
-  | GType s -> interp_level_info loc evd s
+  | GType s -> interp_level_info ?loc evd s
 
-let interp_instance loc evd ~len l =
+let interp_instance ?loc evd ~len l =
   if len != List.length l then
-    user_err ~loc ~hdr:"pretype"
+    user_err ?loc ~hdr:"pretype"
       (str "Universe instance should have length " ++ int len)
   else
     let evd, l' =
       List.fold_left
         (fun (evd, univs) l ->
-	  let evd, l = interp_glob_level loc evd l in
+	  let evd, l = interp_glob_level ?loc evd l in
 	  (evd, l :: univs)) (evd, [])
         l
     in
     if List.exists (fun l -> Univ.Level.is_prop l) l' then
-      user_err ~loc ~hdr:"pretype"
+      user_err ?loc ~hdr:"pretype"
 	(str "Universe instances cannot contain Prop, polymorphic" ++
 	   str " universe instances must be greater or equal to Set.");
     evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
 
-let pretype_global loc rigid env evd gr us = 
+let pretype_global ?loc rigid env evd gr us = 
   let evd, instance = 
     match us with
     | None -> evd, None
     | Some l -> 
        let _, ctx = Universes.unsafe_constr_of_global gr in
        let len = Univ.UContext.size ctx in
-       interp_instance loc evd ~len l
+       interp_instance ?loc evd ~len l
   in
-  let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
+  let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
   (sigma, EConstr.of_constr c)
 
-let pretype_ref loc evdref env ref us =
+let pretype_ref ?loc evdref env ref us =
   match ref with
   | VarRef id ->
       (* Section variable *)
@@ -533,15 +533,15 @@ let pretype_ref loc evdref env ref us =
          (* This may happen if env is a goal env and section variables have
             been cleared - section variables should be different from goal
             variables *)
-         Pretype_errors.error_var_not_found ~loc id)
+         Pretype_errors.error_var_not_found ?loc id)
   | ref ->
-    let evd, c = pretype_global loc univ_flexible env !evdref ref us in
+    let evd, c = pretype_global ?loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
     let ty = unsafe_type_of env.ExtraEnv.env evd c in
       make_judge c ty
 
 let judge_of_Type loc evd s =
-  let evd, s = interp_universe ~loc evd s in
+  let evd, s = interp_universe ?loc evd s in
   let judge = 
     { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
   in
@@ -574,12 +574,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
   let open Context.Rel.Declaration in
   match t with
   | GRef (ref,u) ->
-      inh_conv_coerce_to_tycon ~loc env evdref
-	(pretype_ref loc evdref env ref u)
+      inh_conv_coerce_to_tycon ?loc env evdref
+	(pretype_ref ?loc evdref env ref u)
 	tycon
 
   | GVar id ->
-    inh_conv_coerce_to_tycon ~loc env evdref
+    inh_conv_coerce_to_tycon ?loc env evdref
       (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
       tycon
 
@@ -589,12 +589,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let evk =
         try Evd.evar_key id !evdref
         with Not_found ->
-          user_err ~loc  (str "Unknown existential variable.") in
+          user_err ?loc  (str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
-	inh_conv_coerce_to_tycon ~loc env evdref j tycon
+	inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
   | GPatVar (someta,n) ->
     let env = ltac_interp_name_env k0 lvar env !evdref in
@@ -674,7 +674,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      Typing.check_type_fixpoint ~loc env.ExtraEnv.env evdref names ftys vdefj;
+      Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj;
       let nf c = nf_evar !evdref c in
       let ftys = Array.map nf ftys in (** FIXME *)
       let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
@@ -696,7 +696,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  let fixdecls = (names,ftys,fdefs) in
           let indexes =
             search_guard
-              ~loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls)
+              ?loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls)
           in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
@@ -705,15 +705,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
             (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls)
              with reraise ->
                let (e, info) = CErrors.push reraise in
-               let info = Loc.add_loc info loc in
+               let info = Option.cata (Loc.add_loc info) info loc in
                iraise (e, info));
 	    make_judge (mkCoFix cofix) ftys.(i)
       in
-	inh_conv_coerce_to_tycon ~loc env evdref fixj tycon
+	inh_conv_coerce_to_tycon ?loc env evdref fixj tycon
 
   | GSort s ->
     let j = pretype_sort loc evdref s in
-      inh_conv_coerce_to_tycon ~loc env evdref j tycon
+      inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
   | GApp (f,args) ->
     let fj = pretype empty_tycon env evdref lvar f in
@@ -775,7 +775,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | _ ->
 	    let hj = pretype empty_tycon env evdref lvar c in
 	      error_cant_apply_not_functional
-                ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref
+                ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref
                 resj [|hj|]
     in
     let resj = apply_rec env 1 fj candargs args in
@@ -792,7 +792,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  else resj
       | _ -> resj 
     in
-      inh_conv_coerce_to_tycon ~loc env evdref resj tycon
+      inh_conv_coerce_to_tycon ?loc env evdref resj tycon
 
   | GLambda(name,bk,c1,c2)      ->
     let tycon' = evd_comb1
@@ -800,11 +800,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	match tycon with
 	| None -> evd, tycon
 	| Some ty ->
-	  let evd, ty' = Coercion.inh_coerce_to_prod ~loc env.ExtraEnv.env evd ty in
+	  let evd, ty' = Coercion.inh_coerce_to_prod ?loc env.ExtraEnv.env evd ty in
 	    evd, Some ty')
       evdref tycon
     in
-    let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in
+    let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in
     let dom_valcon = valcon_of_tycon dom in
     let j = pretype_type dom_valcon env evdref lvar c1 in
     (* The name specified by ltac is used also to create bindings. So
@@ -814,7 +814,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in
     let name = ltac_interp_name lvar name in
     let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
-      inh_conv_coerce_to_tycon ~loc env evdref resj tycon
+      inh_conv_coerce_to_tycon ?loc env evdref resj tycon
 
   | GProd(name,bk,c1,c2)        ->
     let j = pretype_type empty_valcon env evdref lvar c1 in
@@ -836,9 +836,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         judge_of_product env.ExtraEnv.env name j j'
       with TypeError _ as e ->
         let (e, info) = CErrors.push e in
-        let info = Loc.add_loc info loc in
+        let info = Option.cata (Loc.add_loc info) info loc in
         iraise (e, info) in
-      inh_conv_coerce_to_tycon ~loc env evdref resj tycon
+      inh_conv_coerce_to_tycon ?loc env evdref resj tycon
 
   | GLetIn(name,c1,t,c2)      ->
     let tycon1 =
@@ -867,15 +867,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj
+	  error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj
     in
     let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
-      user_err ~loc  (str "Destructing let is only for inductive types" ++
+      user_err ?loc  (str "Destructing let is only for inductive types" ++
 	str " with one constructor.");
     let cs = cstrs.(0) in
     if not (Int.equal (List.length nal) cs.cs_nargs) then
-      user_err ~loc:loc (str "Destructing let on this type expects " ++ 
+      user_err ?loc:loc (str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
@@ -944,7 +944,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      if noccur_between !evdref 1 cs.cs_nargs ccl then
 		lift (- cs.cs_nargs) ccl
 	      else
-		error_cant_find_case_type ~loc env.ExtraEnv.env !evdref
+		error_cant_find_case_type ?loc env.ExtraEnv.env !evdref
 		  cj.uj_val in
 		 (* let ccl = refresh_universes ccl in *)
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
@@ -960,10 +960,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in
+	  error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in
     let cstrs = get_constructors env.ExtraEnv.env indf in
       if not (Int.equal (Array.length cstrs) 2) then
-        user_err ~loc 
+        user_err ?loc 
 		      (str "If is only for inductive types with two constructors.");
 
       let arsgn =
@@ -1020,10 +1020,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
       let cj = { uj_val = v; uj_type = p } in
-      inh_conv_coerce_to_tycon ~loc env evdref cj tycon
+      inh_conv_coerce_to_tycon ?loc env evdref cj tycon
 
   | GCases (sty,po,tml,eqns) ->
-    Cases.compile_cases ~loc sty
+    Cases.compile_cases ?loc sty
       ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
       tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
 
@@ -1032,7 +1032,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       match k with
       | CastCoerce ->
 	let cj = pretype empty_tycon env evdref lvar c in
-	  evd_comb1 (Coercion.inh_coerce_to_base ~loc env.ExtraEnv.env) evdref cj
+	  evd_comb1 (Coercion.inh_coerce_to_base ?loc env.ExtraEnv.env) evdref cj
       | CastConv t | CastVM t | CastNative t ->
 	let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
 	let tj = pretype_type empty_valcon env evdref lvar t in
@@ -1048,9 +1048,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
 		if b then (evdref := evd; cj, tval)
 		else
-		  error_actual_type ~loc env.ExtraEnv.env !evdref cj tval 
+		  error_actual_type ?loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
-	      else user_err ~loc  (str "Cannot check cast with vm: " ++
+	      else user_err ?loc  (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
@@ -1059,7 +1059,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
 	      if b then (evdref := evd; cj, tval)
 	      else
-                error_actual_type ~loc env.ExtraEnv.env !evdref cj tval
+                error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
                   (ConversionFailed (env.ExtraEnv.env,cty,tval))
             end
 	  | _ -> 
@@ -1067,7 +1067,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	in
 	let v = mkCast (cj.uj_val, k, tval) in
 	  { uj_val = v; uj_type = tval }
-    in inh_conv_coerce_to_tycon ~loc env evdref cj tycon
+    in inh_conv_coerce_to_tycon ?loc env evdref cj tycon
 
 and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   let f decl (subst,update) =
@@ -1087,7 +1087,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
         let t' = env |> lookup_named id |> NamedDecl.get_type in
         if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
-        user_err ~loc  (str "Cannot interpret " ++
+        user_err ?loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
           str " in current context: no binding for " ++ pr_id id ++ str ".") in
     ((id,c)::subst, update) in
@@ -1128,14 +1128,14 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
   | c ->
       let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
-      let tj = evd_comb1 (Coercion.inh_coerce_to_sort ~loc env.ExtraEnv.env) evdref j in
+      let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in
 	match valcon with
 	| None -> tj
 	| Some v ->
 	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
 	    else
 	      error_unexpected_type
-                ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+                ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let env = make_env env sigma in