From 846b74275511bd89c2f3abe19245133050d2199c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Jan 2017 20:11:01 +0100
Subject: [constrexpr] Make patterns use Loc.located for location information

This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.

Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.

Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.

`git grep 'Loc.t \*'` gives an overview of the remaining work to do.

We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
---
 interp/constrintern.ml | 114 ++++++++++++++++++++++++-------------------------
 1 file changed, 56 insertions(+), 58 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf3..6bf6772c61 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -230,7 +230,7 @@ let contract_pat_notation ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CPatNotation (_,"{ _ }",([a],[]),[]) :: l ->
+    | (_, CPatNotation ("{ _ }",([a],[]),[])) :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -430,17 +430,16 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
-let rec free_vars_of_pat il =
-  function
-  | CPatCstr (loc, c, l1, l2) ->
+let rec free_vars_of_pat il (loc, pt) = match pt with
+  | CPatCstr (c, l1, l2) ->
       let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
       List.fold_left free_vars_of_pat il l2
-  | CPatAtom (loc, ro) ->
+  | CPatAtom ro ->
       begin match ro with
       | Some (Ident (loc, i)) -> (loc, i) :: il
       | Some _ | None -> il
       end
-  | CPatNotation (loc, n, l1, l2) ->
+  | CPatNotation (n, l1, l2) ->
       let il = List.fold_left free_vars_of_pat il (fst l1) in
       List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
   | _ -> anomaly (str "free_vars_of_pat")
@@ -988,10 +987,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out)
+      then let (b,out) = aux i (q,[]) in (b,(Loc.ghost,RCPatAtom(None))::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out)
+      then let (b,out) = aux i (q,l) in (b,(Loc.ghost, RCPatAtom(None))::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1194,14 +1193,14 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let rec subst_pat_iterator y t p = match p with
-  | RCPatAtom (_,id) ->
-    begin match id with Some x when Id.equal x y -> t | _ -> p end
-  | RCPatCstr (loc,id,l1,l2) ->
-     RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
-	       List.map (subst_pat_iterator y t) l2)
-  | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
-  | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
+let rec subst_pat_iterator y t (loc, p) = match p with
+  | RCPatAtom id ->
+    begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ~loc p end
+  | RCPatCstr (id,l1,l2) ->
+     Loc.tag ~loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
+                                    List.map (subst_pat_iterator y t) l2)
+  | RCPatAlias (p,a) -> Loc.tag ~loc @@ RCPatAlias (subst_pat_iterator y t p,a)
+  | RCPatOr pl       -> Loc.tag ~loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
 
 let drop_notations_pattern looked_for =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1250,46 +1249,46 @@ let drop_notations_pattern looked_for =
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
     with Not_found -> None
-  and in_pat top scopes = function
-    | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id)
-    | CPatRecord (loc, l) ->
+  and in_pat top scopes (loc, pt) = match pt with
+    | CPatAlias (p, id) -> Loc.tag ~loc @@ RCPatAlias (in_pat top scopes p, id)
+    | CPatRecord l ->
       let sorted_fields =
-	sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in
+	sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in
       begin match sorted_fields with
-	| None -> RCPatAtom (loc, None)
+	| None -> Loc.tag ~loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
             if !asymmetric_patterns then pl else
-            let pars = List.make n (CPatAtom (loc, None)) in
+            let pars = List.make n (loc, CPatAtom None) in
             List.rev_append pars pl in
 	  match drop_syndef top scopes head pl with
-	    |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
+	    |Some (a,b,c) -> (loc, RCPatCstr(a, b, c))
 	    |None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, head, None, pl) ->
+    | CPatCstr (head, None, pl) ->
       begin
 	match drop_syndef top scopes head pl with
-	  | Some (a,b,c) -> RCPatCstr(loc, a, b, c)
+	  | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr(a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-     | CPatCstr (loc, r, Some expl_pl, pl) ->
+     | CPatCstr (r, Some expl_pl, pl) ->
       let g = try locate (snd (qualid_of_reference r))
 	      with Not_found ->
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
-        RCPatCstr (loc, g, List.map (in_pat false scopes) pl, [])
+        Loc.tag ~loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
       else
         (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
-        RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
+        Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+    | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
       fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
-    | CPatNotation (_,"( _ )",([a],[]),[]) ->
+    | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
-    | CPatNotation (loc, ntn, fullargs,extrargs) ->
+    | CPatNotation (ntn, fullargs,extrargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
       let ((ids',c),df) = Notation.interp_notation loc ntn scopes in
       let (ids',idsl',_) = split_by_type ids' in
@@ -1297,18 +1296,17 @@ let drop_notations_pattern looked_for =
       let substlist = make_subst idsl' argsl in
       let subst = make_subst ids' args in
       in_not top loc scopes (subst,substlist) extrargs c
-    | CPatDelimiters (loc, key, e) ->
+    | CPatDelimiters (key, e) ->
       in_pat top (None,find_delimiters_scope loc key::snd scopes) e
-    | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
-    | CPatAtom (loc, Some id) ->
+    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+    | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
-	  |Some (a,b,c) -> RCPatCstr (loc, a, b, c)
-	  |None -> RCPatAtom (loc, Some (find_pattern_variable id))
+	  | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr (a, b, c)
+	  | None         -> Loc.tag ~loc @@ RCPatAtom (Some (find_pattern_variable id))
       end
-    | CPatAtom (loc,None) -> RCPatAtom (loc,None)
-    | CPatOr (loc, pl) ->
-      RCPatOr (loc,List.map (in_pat top scopes) pl)
+    | CPatAtom None -> Loc.tag ~loc @@ RCPatAtom None
+    | CPatOr pl     -> Loc.tag ~loc @@ RCPatOr (List.map (in_pat top scopes) pl)
     | CPatCast _ ->
       assert false
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
@@ -1322,17 +1320,17 @@ let drop_notations_pattern looked_for =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-	  if Id.equal id ldots_var then RCPatAtom (loc,Some id) else
+	  if Id.equal id ldots_var then Loc.tag ~loc @@ RCPatAtom (Some id) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
       end
     | NRef g ->
       ensure_kind top loc g;
       let (_,argscs) = find_remaining_scopes [] args g in
-      RCPatCstr (loc, g, [], List.map2 (in_pat_sc scopes) argscs args)
+      Loc.tag ~loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      RCPatCstr (loc, g,
+      Loc.tag ~loc @@ RCPatCstr (g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
@@ -1351,7 +1349,7 @@ let drop_notations_pattern looked_for =
          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole _ ->
       let () = assert (List.is_empty args) in
-      RCPatAtom (loc, None)
+      Loc.tag ~loc @@ RCPatAtom None
     | t -> error_invalid_pattern_notation ~loc ()
   in in_pat true
 
@@ -1363,10 +1361,10 @@ let rec intern_pat genv aliases pat =
       (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
   match pat with
-    | RCPatAlias (loc, p, id) ->
+    | loc, RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_pat genv aliases' p
-    | RCPatCstr (loc, head, expl_pl, pl) ->
+    | loc, RCPatCstr (head, expl_pl, pl) ->
       if !asymmetric_patterns then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
@@ -1378,13 +1376,13 @@ let rec intern_pat genv aliases pat =
 	let with_letin, pl2 =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
-    | RCPatAtom (loc, Some id) ->
+    | loc, RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
       (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)])
-    | RCPatAtom (loc, None) ->
+    | loc, RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
       (ids, [asubst, PatVar (loc, alias_of aliases)])
-    | RCPatOr (loc, pl) ->
+    | loc, RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
       let (idsl,pl') = List.split pl' in
@@ -1402,21 +1400,21 @@ let rec intern_pat genv aliases pat =
    of lambdas in the encoding of match in constr. We put this check here and not
    in the parser because it would require to duplicate the levels of the
    [pattern] rule. *)
-let rec check_no_patcast = function
-  | CPatCast (loc,_,_) ->
+let rec check_no_patcast (loc, pt) = match pt with
+  | CPatCast (_,_) ->
      CErrors.user_err ~loc ~hdr:"check_no_patcast"
                            (Pp.strbrk "Casts are not supported here.")
-  | CPatDelimiters(_,_,p)
-  | CPatAlias(_,p,_) -> check_no_patcast p
-  | CPatCstr(_,_,opl,pl) ->
+  | CPatDelimiters(_,p)
+  | CPatAlias(p,_) -> check_no_patcast p
+  | CPatCstr(_,opl,pl) ->
      Option.iter (List.iter check_no_patcast) opl;
      List.iter check_no_patcast pl
-  | CPatOr(_,pl) ->
+  | CPatOr pl ->
      List.iter check_no_patcast pl
-  | CPatNotation(_,_,subst,pl) ->
+  | CPatNotation(_,subst,pl) ->
      check_no_patcast_subst subst;
      List.iter check_no_patcast pl
-  | CPatRecord(_,prl) ->
+  | CPatRecord prl ->
      List.iter (fun (_,p) -> check_no_patcast p) prl
   | CPatAtom _ | CPatPrim _ -> ()
 
@@ -1441,7 +1439,7 @@ let intern_ind_pattern genv scopes pat =
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc
   in
   match no_not with
-    | RCPatCstr (loc, head, expl_pl, pl) ->
+    | loc, RCPatCstr (head, expl_pl, pl) ->
       let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
@@ -1784,7 +1782,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     (ids,List.flatten mpl')
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
-  and intern_eqn n env (loc,lhs,rhs) =
+  and intern_eqn n env (loc,(lhs,rhs)) =
     let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
-- 
cgit v1.2.3


From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Jan 2017 01:27:40 +0100
Subject: [location] Use Loc.located for constr_expr.

This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.

Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
---
 interp/constrintern.ml | 110 ++++++++++++++++++++++++-------------------------
 1 file changed, 55 insertions(+), 55 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6bf6772c61..4af89e1ef7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -217,7 +217,7 @@ let contract_notation ntn (l,ll,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CNotation (_,"{ _ }",([a],[],[])) :: l ->
+    | (_loc, CNotation ("{ _ }",([a],[],[]))) :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -407,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	  let name =
 	    let id =
 	      match ty with
-	      | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
+	      | _, CApp ((_, (_, CRef (Ident (loc,id),_))), _) -> id
 	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
@@ -448,7 +448,7 @@ let intern_local_pattern intern lvar env p =
   List.fold_left
     (fun env (loc, i) ->
        let bk = Default Implicit in
-       let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in
+       let ty = Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
        let n = Name i in
        let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
        env)
@@ -479,7 +479,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let tyc =
         match ty with
         | Some ty -> ty
-        | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
+        | None -> Loc.tag ~loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
       let il = List.map snd (free_vars_of_pat [] p) in
@@ -592,15 +592,15 @@ let rec subordinate_letins letins = function
 
 let terms_of_binders bl =
   let rec term_of_pat = function
-    | PatVar (loc,Name id) -> CRef (Ident (loc,id), None)
+    | PatVar (loc,Name id)   -> Loc.tag ~loc @@ CRef (Ident (loc,id), None)
     | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
     | PatCstr (loc,c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
-       let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in
+       let hole = Loc.tag ~loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
-       CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
+       Loc.tag ~loc @@ CAppExpl ((None,r,None),params @ List.map term_of_pat l) in
   let rec extract_variables = function
-    | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l
+    | GLocalAssum (loc,Name id,_,_)::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
     | GLocalDef (loc,Anonymous,_,_,_)::l
     | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term."
@@ -754,7 +754,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
     let expl_impls = List.map
-      (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+      (fun id -> Loc.tag ~loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -1515,15 +1515,15 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
-  let rec intern env = function
-    | CRef (ref,us) as x ->
+  let rec intern env = Loc.with_loc (fun ~loc -> function
+    | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
-	  intern_applied_reference intern env (Environ.named_context globalenv) 
-	    lvar us [] ref 
+	  intern_applied_reference intern env (Environ.named_context globalenv)
+	    lvar us [] ref
 	in
-	  apply_impargs c env imp subscopes l (constr_loc x)
+	  apply_impargs c env imp subscopes l loc
 
-    | CFix (loc, (locid,iddef), dl) ->
+    | CFix ((locid,iddef), dl) ->
         let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
@@ -1564,7 +1564,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
               Array.map (fun (_,bl,_,_) -> bl) idl,
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
-    | CCoFix (loc, (locid,iddef), dl) ->
+    | CCoFix ((locid,iddef), dl) ->
         let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
@@ -1589,33 +1589,33 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
-    | CProdN (loc,[],c2) ->
+    | CProdN ([],c2) ->
         intern_type env c2
-    | CProdN (loc,(nal,bk,ty)::bll,c2) ->
-        iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
-    | CLambdaN (loc,[],c2) ->
+    | CProdN ((nal,bk,ty)::bll,c2) ->
+        iterate_prod loc env bk ty (Loc.tag ~loc @@ CProdN (bll, c2)) nal
+    | CLambdaN ([],c2) ->
         intern env c2
-    | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
-    | CLetIn (loc,na,c1,t,c2) ->
+    | CLambdaN ((nal,bk,ty)::bll,c2) ->
+	iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ~loc @@ CLambdaN (bll, c2)) nal
+    | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
 	GLetIn (loc, snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
+    | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
-	intern env (CPrim (loc,Numeral (Bigint.neg p)))
-    | CNotation (_,"( _ )",([a],[],[])) -> intern env a
-    | CNotation (loc,ntn,args) ->
+	intern env (Loc.tag ~loc @@ CPrim (Numeral (Bigint.neg p)))
+    | CNotation ("( _ )",([a],[],[])) -> intern env a
+    | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
-    | CGeneralization (loc,b,a,c) ->
+    | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
-    | CPrim (loc, p) ->
+    | CPrim p ->
 	fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
-    | CDelimiters (loc, key, e) ->
+    | CDelimiters (key, e) ->
 	intern {env with tmp_scope = None;
 		  scopes = find_delimiters_scope loc key :: env.scopes} e
-    | CAppExpl (loc, (isproj,ref,us), args) ->
+    | CAppExpl ((isproj,ref,us), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
@@ -1624,42 +1624,42 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  (* Rem: GApp(_,f,[]) stands for @f *)
 	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
 
-    | CApp (loc, (isproj,f), args) ->
+    | CApp ((isproj,f), args) ->
         let f,args = match f with
           (* Compact notations like "t.(f args') args" *)
-          | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> 
+          | _loc, CApp ((Some _,f), args') when not (Option.has_some isproj) ->
 	    f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
           | _ -> f,args in
 	let (c,impargs,args_scopes,l),args =
           match f with
-            | CRef (ref,us) -> 
+            | _loc, CRef (ref,us) -> 
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
-            | CNotation (loc,ntn,([],[],[])) ->
+            | _loc, CNotation (ntn,([],[],[])) ->
                 let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
             | x -> (intern env f,[],[],[]), args in
-          apply_impargs c env impargs args_scopes 
+          apply_impargs c env impargs args_scopes
 	    (merge_impargs l args) loc
 
-    | CRecord (loc, fs) ->
+    | CRecord fs ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
-                                                 Misctypes.IntroAnonymous, None))
+	             (fun _idx -> Loc.tag ~loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+                                                         Misctypes.IntroAnonymous, None))
        in
        begin
 	  match fields with
 	    | None -> user_err ~loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
-                let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
+		let pars = List.make n (Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+                let app = Loc.tag ~loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
 	  intern env app
 	end
-    | CCases (loc, sty, rtnpo, tms, eqns) ->
+    | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
             (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
@@ -1701,7 +1701,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
-    | CLetTuple (loc, nal, (na,po), b, c) ->
+    | CLetTuple (nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
@@ -1711,7 +1711,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  intern_type env'' u) po in
         GLetTuple (loc, List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
-    | CIf (loc, c, (na,po), b1, b2) ->
+    | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
@@ -1719,7 +1719,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
-    | CHole (loc, k, naming, solve) ->
+    | CHole (k, naming, solve) ->
         let k = match k with
         | None ->
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -1745,22 +1745,22 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         in
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar (loc, n) when allow_patvar ->
+    | CPatVar n when allow_patvar ->
 	GPatVar (loc, (true,n))
-    | CEvar (loc, n, []) when allow_patvar ->
+    | CEvar (n, []) when allow_patvar ->
 	GPatVar (loc, (false,n))
     (* end *)
     (* Parsing existential variables *)
-    | CEvar (loc, n, l) ->
+    | CEvar (n, l) ->
 	GEvar (loc, n, List.map (on_snd (intern env)) l)
-    | CPatVar (loc, _) ->
+    | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
-    | CSort (loc, s) ->
+    | CSort s ->
 	GSort(loc,s)
-    | CCast (loc, c1, c2) ->
+    | CCast (c1, c2) ->
         GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
-
+  )
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder env bind =
@@ -1887,17 +1887,17 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  intern_args env subscopes rargs
     in aux 1 l subscopes eargs rargs
 
-  and apply_impargs c env imp subscopes l loc = 
+  and apply_impargs c env imp subscopes l loc =
     let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
     let l = intern_impargs c env imp subscopes l in
       smart_gapp c loc l
 
   and smart_gapp f loc = function
     | [] -> f
-    | l -> match f with 
+    | l -> match f with
       | GApp (loc', g, args) -> GApp (Loc.merge loc' loc, g, args@l)
       | _ -> GApp (Loc.merge (loc_of_glob_constr f) loc, f, l)
-      
+
   and intern_args env subscopes = function
     | [] -> []
     | a::args ->
-- 
cgit v1.2.3


From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Jan 2017 13:02:55 +0100
Subject: [location] Move Glob_term.cases_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.
---
 interp/constrintern.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4af89e1ef7..4960d7332e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -591,14 +591,14 @@ let rec subordinate_letins letins = function
       letins,[]
 
 let terms_of_binders bl =
-  let rec term_of_pat = function
-    | PatVar (loc,Name id)   -> Loc.tag ~loc @@ CRef (Ident (loc,id), None)
-    | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
-    | PatCstr (loc,c,l,_) ->
+  let rec term_of_pat pt = Loc.map_with_loc (fun ~loc -> function
+    | PatVar (Name id)   -> CRef (Ident (loc,id), None)
+    | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
+    | PatCstr (c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
        let hole = Loc.tag ~loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
-       Loc.tag ~loc @@ CAppExpl ((None,r,None),params @ List.map term_of_pat l) in
+       CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
     | GLocalAssum (loc,Name id,_,_)::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
@@ -1015,8 +1015,8 @@ let chop_params_pattern loc ind args with_letin =
     else Inductiveops.inductive_nparams ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
-  List.iter (function PatVar(_,Anonymous) -> ()
-    | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
+  List.iter (function _, PatVar Anonymous -> ()
+    | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
   args
 
 let find_constructor loc add_params ref =
@@ -1036,7 +1036,7 @@ let find_constructor loc add_params ref =
           then Inductiveops.inductive_nparamdecls ind
           else Inductiveops.inductive_nparams ind
       in
-      List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
+      List.make nb ([], [(Id.Map.empty, Loc.tag @@ PatVar Anonymous)])
     | None -> []
 
 let find_pattern_variable = function
@@ -1358,7 +1358,7 @@ let rec intern_pat genv aliases pat =
     let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
     let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
-      (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+      (asubst, Loc.tag ~loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
   match pat with
     | loc, RCPatAlias (p, id) ->
@@ -1378,10 +1378,10 @@ let rec intern_pat genv aliases pat =
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
     | loc, RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
-      (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)])
+      (aliases.alias_ids,[aliases.alias_map, Loc.tag ~loc @@ PatVar (alias_of aliases)])
     | loc, RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
-      (ids, [asubst, PatVar (loc, alias_of aliases)])
+      (ids, [asubst, Loc.tag ~loc @@ PatVar (alias_of aliases)])
     | loc, RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
@@ -1678,14 +1678,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let stripped_match_from_in =
           let rec aux = function
 	    | [] -> []
-	    | (_,PatVar _) :: q -> aux q
+	    | (_, (_loc, PatVar _)) :: q -> aux q
 	    | l -> l
 	  in aux match_from_in in
         let rtnpo = match stripped_match_from_in with
 	  | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
 	  | l ->
              (* Build a return predicate by expansion of the patterns of the "in" clause *)
-             let thevars,thepats = List.split l in
+             let thevars, thepats = List.split l in
              let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
              let sub_tms = List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars (* "match v1,..,vn" *) in
              let main_sub_eqn =
@@ -1695,7 +1695,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
-                 [Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
+                 [Loc.ghost,[],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
 		  GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)]   (* "=> _" *) in
              Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
@@ -1817,14 +1817,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
 	    let add_name l = function
 	      | _,Anonymous -> l
-	      | loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in
+	      | loc,(Name y as x) -> (y, Loc.tag ~loc @@ PatVar x) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
 		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
 	      | [],[] ->
 		(add_name match_acc na, var_acc)
-	      | _::t,PatVar (loc,x)::tt ->
+	      | _::t, (loc, PatVar x)::tt ->
 		canonize_args t tt forbidden_names
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
 	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
-- 
cgit v1.2.3


From be83b52cf50ed4c596e40cfd52da03258a7a4a18 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Jan 2017 13:22:42 +0100
Subject: [location] Move Glob_term.predicate_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4960d7332e..f814205dce 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1836,7 +1836,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
 	  canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
-	match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
+	match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
     | None ->
       [], None in
     (tm',(snd na,typ)), extra_id, match_td
-- 
cgit v1.2.3


From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:23:53 +0100
Subject: [location] Switch glob_constr to Loc.located

---
 interp/constrintern.ml | 147 +++++++++++++++++++++++++++----------------------
 1 file changed, 82 insertions(+), 65 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f814205dce..cc7203ac00 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -304,12 +304,12 @@ let reset_tmp_scope env = {env with tmp_scope = None}
 
 let rec it_mkGProd loc2 env body =
   match env with
-      (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GProd (na, bk, t, body))
     | [] -> body
 
 let rec it_mkGLambda loc2 env body =
   match env with
-      (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GLambda (na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -322,14 +322,14 @@ let build_impls = function
 
 let impls_type_list ?(args = []) =
   let rec aux acc = function
-    |GProd (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+    |_, GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
     |_ -> (Variable,[],List.append args (List.rev acc),[])
   in aux []
 
 let impls_term_list ?(args = []) =
   let rec aux acc = function
-    |GLambda (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
-    |GRec (_, fix_kind, nas, args, tys, bds) ->
+    |_, GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+    |_, GRec (fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
 	 aux acc' bds.(nb)
@@ -346,12 +346,12 @@ let rec check_capture ty = function
       ()
 
 let locate_if_hole loc na = function
-  | GHole (_,_,naming,arg) ->
+  | _, GHole (_,naming,arg) ->
       (try match na with
 	| Name id -> glob_constr_of_notation_constr loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> GHole (loc, Evar_kinds.BinderType na, naming, arg))
+      with Not_found -> Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -397,7 +397,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
     env fvs in
   let bl = List.map
     (fun (id, loc) ->
-      (loc, (Name id, b, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+      (loc, (Name id, b, Loc.tag ~loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -458,7 +458,7 @@ let glob_local_binder_of_extended = function
   | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
   | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t)
   | GLocalDef (loc,na,bk,c,None) ->
-      let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+      let t = Loc.tag ~loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
       (na,bk,Some c,t)
   | GLocalPattern (loc,_,_,_,_) ->
       Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
@@ -517,10 +517,12 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            Loc.tag ~loc:(Loc.merge loc' loc) @@
+	    GProd (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
 	else
 	  (fun (id, loc') acc ->
-	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            Loc.tag ~loc:(Loc.merge loc' loc) @@
+	    GLambda (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -572,10 +574,10 @@ let make_letins =
     (fun a c ->
      match a with
      | LPLetIn (loc,(na,b,t)) ->
-         GLetIn(loc,na,b,t,c)
+       Loc.tag ~loc @@ GLetIn(na,b,t,c)
      | LPCases (loc,(cp,il),id) ->
-         let tt = (GVar(loc,id),(Name id,None)) in
-         GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
+         let tt = (Loc.tag ~loc @@ GVar id, (Name id,None)) in
+         Loc.tag ~loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
 
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
@@ -660,7 +662,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let bindings = Id.Map.map mk_env terms in
         Some (Genintern.generic_substitute_notation bindings arg)
       in
-      GHole (loc, knd, naming, arg)
+      Loc.tag ~loc @@ GHole (knd, naming, arg)
     | NBinderList (x,y,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -678,22 +680,22 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
         let (loc,(na,bk,t)) = a in
-        GProd (loc,na,bk,t,e)
+        Loc.tag ~loc @@ GProd (na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let (loc,(na,bk,t)) = a in
-        GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+        Loc.tag ~loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
-	GProd (loc,na,Explicit,ty,aux subst' subinfos c')
+        let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	Loc.tag ~loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
     | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
-	GLambda (loc,na,Explicit,ty,aux subst' subinfos c')
+        let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	Loc.tag ~loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
     | t ->
       glob_constr_of_notation_constr_with_binders loc
         (traverse_binder subst avoid) (aux subst') subinfos t
@@ -705,11 +707,12 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       intern {env with tmp_scope = scopt;
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
+    Loc.tag ~loc (
     try
-      GVar (loc, Id.Map.find id renaming)
+      GVar (Id.Map.find id renaming)
     with Not_found ->
       (* Happens for local notation joint with inductive/fixpoint defs *)
-      GVar (loc,id)
+      GVar id)
   in aux (terms,None,None) infos c
 
 let split_by_type ids =
@@ -744,7 +747,7 @@ let string_of_ty = function
   | Variable -> "var"
 
 let gvar (loc, id) us = match us with
-| None -> GVar (loc, id)
+| None -> Loc.tag ~loc @@ GVar id
 | Some _ ->
   user_err ~loc  (str "Variable " ++ pr_id id ++
     str " cannot have a universe instance")
@@ -786,25 +789,25 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	GRef (loc, ref, us), impls, scopes, []
+	Loc.tag ~loc @@ GRef (ref, us), impls, scopes, []
       with e when CErrors.noncritical e ->
 	(* [id] a goal variable *)
 	gvar (loc,id) us, [], [], []
 
 let find_appl_head_data c =
-  match c with
-  | GRef (loc,ref,_) as x -> 
+  match Loc.obj c with
+  | GRef (ref,_) ->
     let impls = implicits_of_global ref in
     let scopes = find_arguments_scope ref in
-      x, impls, scopes, []
-  | GApp (_,GRef (_,ref,_),l) as x
+      c, impls, scopes, []
+  | GApp ((_, GRef (ref,_)),l)
       when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       let impls = implicits_of_global ref in 
       let scopes = find_arguments_scope ref in
-	x, List.map (drop_first_implicits n) impls,
+	c, List.map (drop_first_implicits n) impls,
 	List.skipn_at_least n scopes,[]
-  | x -> x,[],[],[]
+  | _ -> c,[],[],[]
 
 let error_not_enough_arguments loc =
   user_err ~loc  (str "Abbreviation is not applied enough.")
@@ -836,7 +839,7 @@ let intern_reference ref =
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env lvar us args =
   match intern_extended_global_of_qualid (loc,qid) with
-  | TrueGlobal ref -> GRef (loc, ref, us), true, args
+  | TrueGlobal ref -> (Loc.tag ~loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
@@ -850,9 +853,9 @@ let intern_qualid loc qid intern env lvar us args =
       let c = instantiate_notation_constr loc intern lvar subst infos c in
       let c = match us, c with
       | None, _ -> c
-      | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
-      | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
-         GApp (loc, GRef (loc', ref, us), arg)
+      | Some _, (loc, GRef (ref, None)) -> Loc.tag ~loc @@ GRef (ref, us)
+      | Some _, (loc, GApp ((loc', GRef (ref, None)), arg)) ->
+        Loc.tag ~loc @@ GApp (Loc.tag ~loc:loc' @@ GRef (ref, us), arg)
       | Some _, _ ->
         user_err ~loc  (str "Notation " ++ pr_qualid qid ++
           str " cannot have a universe instance, its expanded head
@@ -863,7 +866,7 @@ let intern_qualid loc qid intern env lvar us args =
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar us args =
   match intern_qualid loc qid intern env lvar us args with
-    | GRef (_, VarRef _, _),_,_ -> raise Not_found
+    | (_, GRef (VarRef _, _)),_,_ -> raise Not_found
     | r -> r
 
 let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
@@ -1470,8 +1473,8 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
-  | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+  | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+  | (loc, GVar id) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
@@ -1558,7 +1561,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
-	GRec (loc,GFix
+	Loc.tag ~loc @@
+          GRec (GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
               Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -1584,7 +1588,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
-	GRec (loc,GCoFix n,
+	Loc.tag ~loc @@
+	GRec (GCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
@@ -1600,7 +1605,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
-	GLetIn (loc, snd na, inc1, int,
+	Loc.tag ~loc @@
+	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
@@ -1622,7 +1628,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    lvar us args ref 
 	in
 	  (* Rem: GApp(_,f,[]) stands for @f *)
-	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
+	Loc.tag ~loc @@
+	  GApp (f, intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
         let f,args = match f with
@@ -1687,20 +1694,21 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
              (* Build a return predicate by expansion of the patterns of the "in" clause *)
              let thevars, thepats = List.split l in
              let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
-             let sub_tms = List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars (* "match v1,..,vn" *) in
-             let main_sub_eqn =
-               (Loc.ghost,[],thepats, (* "|p1,..,pn" *)
+             let sub_tms = List.map (fun id -> (Loc.tag @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
+             let main_sub_eqn = Loc.tag @@
+               ([],thepats, (* "|p1,..,pn" *)
 		Option.cata (intern_type env')
-                  (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+                  (Loc.tag ~loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
-                 [Loc.ghost,[],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
-		  GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)]   (* "=> _" *) in
-             Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+                  [Loc.tag @@ ([],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
+                   Loc.tag @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
+             Some (Loc.tag @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
+	Loc.tag ~loc @@
+	GCases (sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
@@ -1709,7 +1717,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.ghost,na') in
 	  intern_type env'' u) po in
-        GLetTuple (loc, List.map snd nal, (na', p'), b',
+	Loc.tag ~loc @@
+        GLetTuple (List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
@@ -1718,7 +1727,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
-        GIf (loc, c', (na', p'), intern env b1, intern env b2)
+	Loc.tag ~loc @@
+        GIf (c', (na', p'), intern env b1, intern env b2)
     | CHole (k, naming, solve) ->
         let k = match k with
         | None ->
@@ -1743,23 +1753,29 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
         in
-	GHole (loc, k, naming, solve)
+	Loc.tag ~loc @@
+	GHole (k, naming, solve)
     (* Parsing pattern variables *)
     | CPatVar n when allow_patvar ->
-	GPatVar (loc, (true,n))
+	Loc.tag ~loc @@
+	GPatVar (true,n)
     | CEvar (n, []) when allow_patvar ->
-	GPatVar (loc, (false,n))
+	Loc.tag ~loc @@
+	GPatVar (false,n)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (n, l) ->
-	GEvar (loc, n, List.map (on_snd (intern env)) l)
+	Loc.tag ~loc @@
+	GEvar (n, List.map (on_snd (intern env)) l)
     | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
     | CSort s ->
-	GSort(loc,s)
+	Loc.tag ~loc @@
+	GSort s
     | CCast (c1, c2) ->
-        GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
+	Loc.tag ~loc @@
+        GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
   )
   and intern_type env = intern (set_type_scope env)
 
@@ -1790,15 +1806,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
       let rhs' = intern {env with ids = env_ids} rhs in
-      (loc,eqn_ids,pl,rhs')) pll
+      (loc,(eqn_ids,pl,rhs'))) pll
 
   and intern_case_item env forbidden_names_for_gen (tm,na,t) =
     (* the "match" part *)
     let tm' = intern env tm in
     (* the "as" part *)
     let extra_id,na = match tm', na with
-      | GVar (loc,id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
-      | GRef (loc, VarRef id, _), None -> Some id,(loc,Name id)
+      | (loc , GVar id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
+      | (loc, GRef (VarRef id, _)), None -> Some id,(loc,Name id)
       | _, None -> None,(Loc.ghost,Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
     (* the "in" part *)
@@ -1870,8 +1886,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
             (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
-	    GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
-	      aux (n+1) impl' subscopes' eargs rargs
+              (Loc.map (fun (a,b,c) -> GHole(a,b,c))
+                (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c)
+              ) :: aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
 	  intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
@@ -1895,8 +1912,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   and smart_gapp f loc = function
     | [] -> f
     | l -> match f with
-      | GApp (loc', g, args) -> GApp (Loc.merge loc' loc, g, args@l)
-      | _ -> GApp (Loc.merge (loc_of_glob_constr f) loc, f, l)
+      | (loc', GApp (g, args)) -> Loc.tag ~loc:(Loc.merge loc' loc) @@ GApp (g, args@l)
+      | _ -> Loc.tag ~loc:(Loc.merge (loc_of_glob_constr f) loc) @@ GApp (f, l)
 
   and intern_args env subscopes = function
     | [] -> []
-- 
cgit v1.2.3


From a9d151a31937724543d5269e72b0262c8764c46e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:44:28 +0100
Subject: [location] More located use.

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cc7203ac00..d1b931a227 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -475,7 +475,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
      let ty = Option.map (intern env) ty in
       (push_name_env lvar (impls_term_list term) env locna,
        GLocalDef (loc,na,Explicit,term,ty) :: bl)
-  | CLocalPattern (loc,p,ty) ->
+  | CLocalPattern (loc,(p,ty)) ->
       let tyc =
         match ty with
         | Some ty -> ty
-- 
cgit v1.2.3


From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 interp/constrintern.ml | 99 ++++++++++++++++++++++++++------------------------
 1 file changed, 51 insertions(+), 48 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d1b931a227..585f038086 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -345,13 +345,13 @@ let rec check_capture ty = function
   | [] ->
       ()
 
-let locate_if_hole loc na = function
+let locate_if_hole ?loc na = function
   | _, GHole (_,naming,arg) ->
       (try match na with
-	| Name id -> glob_constr_of_notation_constr loc
+	| Name id -> glob_constr_of_notation_constr ?loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
+      with Not_found -> Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -424,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty =
       List.fold_left
 	(fun (env, bl) (loc, na as locna) ->
           (push_name_env lvar impls env locna,
-           (loc,(na,k,locate_if_hole loc na ty))::bl))
+           (loc,(na,k,locate_if_hole ~loc na ty))::bl))
 	(env, []) nal
   | Generalized (b,b',t) ->
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
@@ -454,27 +454,28 @@ let intern_local_pattern intern lvar env p =
        env)
     env (free_vars_of_pat [] p)
 
-let glob_local_binder_of_extended = function
-  | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
-  | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t)
-  | GLocalDef (loc,na,bk,c,None) ->
+let glob_local_binder_of_extended = Loc.with_loc (fun ~loc -> function
+  | GLocalAssum (na,bk,t) -> (na,bk,None,t)
+  | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
+  | GLocalDef (na,bk,c,None) ->
       let t = Loc.tag ~loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
       (na,bk,Some c,t)
-  | GLocalPattern (loc,_,_,_,_) ->
+  | GLocalPattern (_,_,_,_) ->
       Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
+  )
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
 
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
-      let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in
+      let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ~loc @@ GLocalAssum (na,c,t)) bl' in
       env, bl' @ bl
   | CLocalDef((loc,na as locna),def,ty) ->
      let term = intern env def in
      let ty = Option.map (intern env) ty in
       (push_name_env lvar (impls_term_list term) env locna,
-       GLocalDef (loc,na,Explicit,term,ty) :: bl)
+       (Loc.tag ~loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
   | CLocalPattern (loc,(p,ty)) ->
       let tyc =
         match ty with
@@ -494,7 +495,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
       let _,(_,bk,t) = List.hd bl' in
-      (env, GLocalPattern(loc,(cp,il),id,bk,t) :: bl)
+      (env, (Loc.tag ~loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -582,13 +583,13 @@ let make_letins =
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
-  | GLocalDef (loc,na,_,b,t)::l ->
+  | (loc, GLocalDef (na,_,b,t))::l ->
       subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l
-  | GLocalAssum (loc,na,bk,t)::l ->
+  | (loc, GLocalAssum (na,bk,t))::l ->
       let letins',rest = subordinate_letins [] l in
       letins',((loc,(na,bk,t)),letins)::rest
-  | GLocalPattern (loc,u,id,bk,t) :: l ->
-      subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l)
+  | (loc, GLocalPattern (u,id,bk,t)) :: l ->
+      subordinate_letins (LPCases (loc,u,id)::letins) ([Loc.tag ~loc @@ GLocalAssum (Name id,bk,t)] @ l)
   | [] ->
       letins,[]
 
@@ -602,11 +603,11 @@ let terms_of_binders bl =
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
-    | GLocalAssum (loc,Name id,_,_)::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
-    | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
-    | GLocalDef (loc,Anonymous,_,_,_)::l
-    | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term."
-    | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l
+    | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+    | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
+    | (loc, GLocalDef (Anonymous,_,_,_))::l
+    | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
+    | (loc, GLocalPattern ((u,_),_,_,_)) :: l -> term_of_pat u :: extract_variables l
     | [] -> [] in
   extract_variables bl
 
@@ -697,7 +698,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
 	Loc.tag ~loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
     | t ->
-      glob_constr_of_notation_constr_with_binders loc
+      glob_constr_of_notation_constr_with_binders ~loc
         (traverse_binder subst avoid) (aux subst') subinfos t
   and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
@@ -728,7 +729,7 @@ let make_subst ids l =
 
 let intern_notation intern env lvar loc ntn fullargs =
   let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
-  let ((ids,c),df) = interp_notation loc ntn (env.tmp_scope,env.scopes) in
+  let ((ids,c),df) = interp_notation ~loc ntn (env.tmp_scope,env.scopes) in
   Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
   let ids,idsl,idsbl = split_by_type ids in
   let terms = make_subst ids args in
@@ -809,8 +810,8 @@ let find_appl_head_data c =
 	List.skipn_at_least n scopes,[]
   | _ -> c,[],[],[]
 
-let error_not_enough_arguments loc =
-  user_err ~loc  (str "Abbreviation is not applied enough.")
+let error_not_enough_arguments ?loc =
+  user_err ?loc  (str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let is_unset (a, b) = match b with None -> false | Some _ -> true in
@@ -843,7 +844,7 @@ let intern_qualid loc qid intern env lvar us args =
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
-      if List.length args < nids then error_not_enough_arguments loc;
+      if List.length args < nids then error_not_enough_arguments ~loc;
       let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
       let terms = make_subst ids (List.map fst args1) in
@@ -893,7 +894,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
-    intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
+    intern_applied_reference (fun _ -> error_not_enough_arguments ?loc:None)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
       (vars, Id.Map.empty) None [] r
@@ -990,10 +991,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,(Loc.ghost,RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,[]) in (b,(Loc.tag @@ RCPatAtom(None))::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,(Loc.ghost, RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,l) in (b,(Loc.tag @@ RCPatAtom(None))::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1239,7 +1240,7 @@ let drop_notations_pattern looked_for =
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	      test_kind top g;
 	      let nvars = List.length vars in
-	      if List.length pats < nvars then error_not_enough_arguments loc;
+	      if List.length pats < nvars then error_not_enough_arguments ~loc;
 	      let pats1,pats2 = List.chop nvars pats in
 	      let subst = make_subst vars pats1 in
 	      let idspl1 = List.map (in_not false loc scopes (subst, Id.Map.empty) []) args in
@@ -1288,20 +1289,20 @@ let drop_notations_pattern looked_for =
         Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
-      fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+      fst (Notation.interp_prim_token_cases_pattern_expr ~loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (ntn, fullargs,extrargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
-      let ((ids',c),df) = Notation.interp_notation loc ntn scopes in
+      let ((ids',c),df) = Notation.interp_notation ~loc ntn scopes in
       let (ids',idsl',_) = split_by_type ids' in
       Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
       let substlist = make_subst idsl' argsl in
       let subst = make_subst ids' args in
       in_not top loc scopes (subst,substlist) extrargs c
     | CPatDelimiters (key, e) ->
-      in_pat top (None,find_delimiters_scope loc key::snd scopes) e
-    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+      in_pat top (None,find_delimiters_scope ~loc key::snd scopes) e
+    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ~loc (test_kind false) p scopes)
     | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
@@ -1540,7 +1541,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       let before, after = split_at_annot bl n in
 	       let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
 	       let ro = f (intern env') in
-	       let n' = Option.map (fun _ -> List.count (function GLocalAssum _ -> true | _ -> false (* remove let-ins *)) rbefore) n in
+	       let n' = Option.map (fun _ -> List.count (function | _, GLocalAssum _ -> true
+                                                                  | _ -> false (* remove let-ins *))
+                        rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, (env',rbl) =
@@ -1559,7 +1562,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
-					    en (Loc.ghost, Name name)) 0 env' lf in
+					    en (Loc.tag @@ Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
 	Loc.tag ~loc @@
           GRec (GFix
@@ -1586,7 +1589,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
-					    en (Loc.ghost, Name name)) 0 env' lf in
+					    en (Loc.tag @@ Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
 	Loc.tag ~loc @@
 	GRec (GCoFix n,
@@ -1617,10 +1620,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
     | CPrim p ->
-	fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
+	fst (Notation.interp_prim_token ~loc p (env.tmp_scope,env.scopes))
     | CDelimiters (key, e) ->
 	intern {env with tmp_scope = None;
-		  scopes = find_delimiters_scope loc key :: env.scopes} e
+		  scopes = find_delimiters_scope ~loc key :: env.scopes} e
     | CAppExpl ((isproj,ref,us), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
@@ -1679,7 +1682,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
 	  tms ([],Id.Set.empty,[]) in
         let env' = Id.Set.fold
-	  (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var))
+	  (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.tag @@ Name var))
 	  (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
         (* PatVars before a real pattern do not need to be matched *)
         let stripped_match_from_in =
@@ -1715,7 +1718,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
-	    (Loc.ghost,na') in
+	    (Loc.tag na') in
 	  intern_type env'' u) po in
 	Loc.tag ~loc @@
         GLetTuple (List.map snd nal, (na', p'), b',
@@ -1725,7 +1728,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
-	    (Loc.ghost,na') in
+	    (Loc.tag na') in
 	  intern_type env'' p) po in
 	Loc.tag ~loc @@
         GIf (c', (na', p'), intern env b1, intern env b2)
@@ -1779,7 +1782,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   )
   and intern_type env = intern (set_type_scope env)
 
-  and intern_local_binder env bind =
+  and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
     intern_local_binder_aux intern ntnvars env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
@@ -1815,7 +1818,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     let extra_id,na = match tm', na with
       | (loc , GVar id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
       | (loc, GRef (VarRef id, _)), None -> Some id,(loc,Name id)
-      | _, None -> None,(Loc.ghost,Anonymous)
+      | _, None -> None,(Loc.tag Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
     (* the "in" part *)
     let match_td,typ = match t with
@@ -1837,7 +1840,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
-		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
+		canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc)
 	      | [],[] ->
 		(add_name match_acc na, var_acc)
 	      | _::t, (loc, PatVar x)::tt ->
@@ -2052,12 +2055,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
 
 let interp_binder env sigma na t =
   let t = intern_gen IsType env t in
-  let t' = locate_if_hole (loc_of_glob_constr t) na t in
+  let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
   understand ~expected_type:IsType env sigma t'
 
 let interp_binder_evars env evdref na t =
   let t = intern_gen IsType env t in
-  let t' = locate_if_hole (loc_of_glob_constr t) na t in
+  let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
   understand_tcc_evars env evdref ~expected_type:IsType t'
 
 open Environ
@@ -2084,7 +2087,7 @@ let interp_rawcontext_evars env evdref k bl =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
        let t' =
-	 if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t
+	 if Option.is_empty b then locate_if_hole ~loc:(loc_of_glob_constr t) na t
 	 else t
        in
        let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
-- 
cgit v1.2.3


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.
---
 interp/constrintern.ml | 338 +++++++++++++++++++++++++------------------------
 1 file changed, 170 insertions(+), 168 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 585f038086..a672771b14 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -118,7 +118,7 @@ type internalization_error =
   | NonLinearPattern of Id.t
   | BadPatternsNumber of int * int
 
-exception InternalizationError of Loc.t * internalization_error
+exception InternalizationError of internalization_error Loc.located
 
 let explain_variable_capture id id' =
   pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++
@@ -271,7 +271,7 @@ let error_expect_binder_notation_type ?loc id =
    (pr_id id ++
     str " is expected to occur in binding position in the right-hand side.")
 
-let set_var_scope loc id istermvar env ntnvars =
+let set_var_scope ?loc id istermvar env ntnvars =
   try
     let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in
     if istermvar then isonlybinding := false;
@@ -282,12 +282,12 @@ let set_var_scope loc id istermvar env ntnvars =
       | Some (tmp, scope) ->
         let s1 = make_current_scope tmp scope in
         let s2 = make_current_scope env.tmp_scope env.scopes in
-        if not (List.equal String.equal s1 s2) then error_inconsistent_scope ~loc id s1 s2
+        if not (List.equal String.equal s1 s2) then error_inconsistent_scope ?loc id s1 s2
       end
     in
     match typ with
     | NtnInternTypeBinder ->
-	if istermvar then error_expect_binder_notation_type ~loc id
+	if istermvar then error_expect_binder_notation_type ?loc id
     | NtnInternTypeConstr ->
 	(* We need sometimes to parse idents at a constr level for
 	   factorization and we cannot enforce this constraint:
@@ -302,14 +302,14 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
-let rec it_mkGProd loc2 env body =
+let rec it_mkGProd ?loc env body =
   match env with
-      (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GProd (na, bk, t, body))
+      (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
     | [] -> body
 
-let rec it_mkGLambda loc2 env body =
+let rec it_mkGLambda ?loc env body =
   match env with
-      (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GLambda (na, bk, t, body))
+      (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -371,15 +371,15 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
   function
   | loc,Anonymous ->
       if global_level then
-	user_err ~loc  (str "Anonymous variables not allowed");
+	user_err ?loc (str "Anonymous variables not allowed");
       env
   | loc,Name id ->
       check_hidden_implicit_parameters id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
-        then error_ldots_var ~loc;
-      set_var_scope loc id false env ntnvars;
+        then error_ldots_var ?loc;
+      set_var_scope ?loc id false env ntnvars;
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
-      else Dumpglob.dump_binding loc id;
+      else Dumpglob.dump_binding ?loc id;
       {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
 let intern_generalized_binder ?(global_level=false) intern_type lvar
@@ -393,11 +393,11 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left
-    (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
+    (fun env (l, x) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
     env fvs in
   let bl = List.map
-    (fun (id, loc) ->
-      (loc, (Name id, b, Loc.tag ~loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+    (fun (loc, id) ->
+      (loc, (Name id, b, Loc.tag ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -424,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty =
       List.fold_left
 	(fun (env, bl) (loc, na as locna) ->
           (push_name_env lvar impls env locna,
-           (loc,(na,k,locate_if_hole ~loc na ty))::bl))
+           (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl))
 	(env, []) nal
   | Generalized (b,b',t) ->
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
@@ -448,20 +448,20 @@ let intern_local_pattern intern lvar env p =
   List.fold_left
     (fun env (loc, i) ->
        let bk = Default Implicit in
-       let ty = Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
+       let ty = Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
        let n = Name i in
        let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
        env)
     env (free_vars_of_pat [] p)
 
-let glob_local_binder_of_extended = Loc.with_loc (fun ~loc -> function
+let glob_local_binder_of_extended = Loc.with_loc (fun ?loc -> function
   | GLocalAssum (na,bk,t) -> (na,bk,None,t)
   | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
   | GLocalDef (na,bk,c,None) ->
-      let t = Loc.tag ~loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+      let t = Loc.tag ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
       (na,bk,Some c,t)
   | GLocalPattern (_,_,_,_) ->
-      Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
+      Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
   )
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
@@ -469,18 +469,18 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd"
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
-      let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ~loc @@ GLocalAssum (na,c,t)) bl' in
+      let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ?loc @@ GLocalAssum (na,c,t)) bl' in
       env, bl' @ bl
   | CLocalDef((loc,na as locna),def,ty) ->
      let term = intern env def in
      let ty = Option.map (intern env) ty in
       (push_name_env lvar (impls_term_list term) env locna,
-       (Loc.tag ~loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
+       (Loc.tag ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
   | CLocalPattern (loc,(p,ty)) ->
       let tyc =
         match ty with
         | Some ty -> ty
-        | None -> Loc.tag ~loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+        | None -> Loc.tag ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
       let il = List.map snd (free_vars_of_pat [] p) in
@@ -495,7 +495,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
       let _,(_,bk,t) = List.hd bl' in
-      (env, (Loc.tag ~loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
+      (env, (Loc.tag ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -517,15 +517,15 @@ let intern_generalization intern env lvar loc bk ak c =
           | None -> false
       in
 	if pi then
-	  (fun (id, loc') acc ->
-            Loc.tag ~loc:(Loc.merge loc' loc) @@
-	    GProd (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+	  (fun (loc', id) acc ->
+            Loc.tag ?loc:(Loc.merge_opt loc' loc) @@
+	    GProd (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
 	else
-	  (fun (id, loc') acc ->
-            Loc.tag ~loc:(Loc.merge loc' loc) @@
-	    GLambda (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+	  (fun (loc', id) acc ->
+            Loc.tag ?loc:(Loc.merge_opt loc' loc) @@
+	    GLambda (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
     in
-      List.fold_right (fun (id, loc as lid) (env, acc) ->
+      List.fold_right (fun (loc, id as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
 	  (env', abs lid acc)) fvs (env,c)
   in c'
@@ -566,44 +566,46 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
     in
     (renaming',env), Name id'
 
-type letin_param =
-  | LPLetIn of Loc.t * (Name.t * glob_constr * glob_constr option)
-  | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t
+type letin_param_r =
+  | LPLetIn of Name.t * glob_constr * glob_constr option
+  | LPCases of (cases_pattern * Id.t list) * Id.t
+and letin_param = letin_param_r Loc.located
 
 let make_letins =
   List.fold_right
     (fun a c ->
      match a with
-     | LPLetIn (loc,(na,b,t)) ->
-       Loc.tag ~loc @@ GLetIn(na,b,t,c)
-     | LPCases (loc,(cp,il),id) ->
-         let tt = (Loc.tag ~loc @@ GVar id, (Name id,None)) in
-         Loc.tag ~loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
+     | loc, LPLetIn (na,b,t) ->
+       Loc.tag ?loc @@ GLetIn(na,b,t,c)
+     | loc, LPCases ((cp,il),id) ->
+         let tt = (Loc.tag ?loc @@ GVar id, (Name id,None)) in
+         Loc.tag ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
 
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
   | (loc, GLocalDef (na,_,b,t))::l ->
-      subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l
+      subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l
   | (loc, GLocalAssum (na,bk,t))::l ->
       let letins',rest = subordinate_letins [] l in
       letins',((loc,(na,bk,t)),letins)::rest
   | (loc, GLocalPattern (u,id,bk,t)) :: l ->
-      subordinate_letins (LPCases (loc,u,id)::letins) ([Loc.tag ~loc @@ GLocalAssum (Name id,bk,t)] @ l)
+      subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins)
+                          ([Loc.tag ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
   | [] ->
       letins,[]
 
 let terms_of_binders bl =
-  let rec term_of_pat pt = Loc.map_with_loc (fun ~loc -> function
+  let rec term_of_pat pt = Loc.map_with_loc (fun ?loc -> function
     | PatVar (Name id)   -> CRef (Ident (loc,id), None)
     | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
     | PatCstr (c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
-       let hole = Loc.tag ~loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+       let hole = Loc.tag ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
-    | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+    | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
     | (loc, GLocalDef (Anonymous,_,_,_))::l
     | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
@@ -663,7 +665,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let bindings = Id.Map.map mk_env terms in
         Some (Genintern.generic_substitute_notation bindings arg)
       in
-      Loc.tag ~loc @@ GHole (knd, naming, arg)
+      Loc.tag ?loc @@ GHole (knd, naming, arg)
     | NBinderList (x,y,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -681,24 +683,24 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
         let (loc,(na,bk,t)) = a in
-        Loc.tag ~loc @@ GProd (na,bk,t,e)
+        Loc.tag ?loc @@ GProd (na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let (loc,(na,bk,t)) = a in
-        Loc.tag ~loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
+        Loc.tag ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-	Loc.tag ~loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
+        let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	Loc.tag ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
     | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-	Loc.tag ~loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
+        let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	Loc.tag ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
     | t ->
-      glob_constr_of_notation_constr_with_binders ~loc
+      glob_constr_of_notation_constr_with_binders ?loc
         (traverse_binder subst avoid) (aux subst') subinfos t
   and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
@@ -708,7 +710,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       intern {env with tmp_scope = scopt;
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
-    Loc.tag ~loc (
+    Loc.tag ?loc (
     try
       GVar (Id.Map.find id renaming)
     with Not_found ->
@@ -729,8 +731,8 @@ let make_subst ids l =
 
 let intern_notation intern env lvar loc ntn fullargs =
   let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
-  let ((ids,c),df) = interp_notation ~loc ntn (env.tmp_scope,env.scopes) in
-  Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
+  let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in
+  Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df;
   let ids,idsl,idsbl = split_by_type ids in
   let terms = make_subst ids args in
   let termlists = make_subst idsl argslist in
@@ -748,9 +750,9 @@ let string_of_ty = function
   | Variable -> "var"
 
 let gvar (loc, id) us = match us with
-| None -> Loc.tag ~loc @@ GVar id
+| None -> Loc.tag ?loc @@ GVar id
 | Some _ ->
-  user_err ~loc  (str "Variable " ++ pr_id id ++
+  user_err ?loc  (str "Variable " ++ pr_id id ++
     str " cannot have a universe instance")
 
 let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
@@ -758,9 +760,9 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
     let expl_impls = List.map
-      (fun id -> Loc.tag ~loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+      (fun id -> Loc.tag ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
-    Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
+    Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
@@ -770,15 +772,15 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
-    (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
+    (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
   (* Is [id] the special variable for recursive notations *)
   else if Id.equal id ldots_var
   then if Id.Map.is_empty ntnvars
-    then error_ldots_var ~loc
+    then error_ldots_var ?loc
     else gvar (loc,id) us, [], [], []
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
-    user_err ~loc ~hdr:"intern_var"
+    user_err ?loc ~hdr:"intern_var"
      (str "variable " ++ pr_id id ++ str " should be bound to a term.")
   else
     (* Is [id] a goal or section variable *)
@@ -789,8 +791,8 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
 	let ref = VarRef id in
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
-	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	Loc.tag ~loc @@ GRef (ref, us), impls, scopes, []
+	Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
+	Loc.tag ?loc @@ GRef (ref, us), impls, scopes, []
       with e when CErrors.noncritical e ->
 	(* [id] a goal variable *)
 	gvar (loc,id) us, [], [], []
@@ -820,11 +822,11 @@ let check_no_explicitation l =
   | [] -> ()
   | (_, None) :: _ -> assert false
   | (_, Some (loc, _)) :: _ ->
-    user_err ~loc  (str"Unexpected explicitation of the argument of an abbreviation.")
+    user_err ?loc  (str"Unexpected explicitation of the argument of an abbreviation.")
 
 let dump_extended_global loc = function
-  | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref
-  | SynDef sp -> Dumpglob.add_glob_kn loc sp
+  | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
+  | SynDef sp -> Dumpglob.add_glob_kn ?loc sp
 
 let intern_extended_global_of_qualid (loc,qid) =
   let r = Nametab.locate_extended qid in dump_extended_global loc r; r
@@ -833,18 +835,18 @@ let intern_reference ref =
   let qid = qualid_of_reference ref in
   let r =
     try intern_extended_global_of_qualid qid
-    with Not_found -> error_global_not_found ~loc:(fst qid) (snd qid)
+    with Not_found -> error_global_not_found ?loc:(fst qid) (snd qid)
   in
   Smartlocate.global_of_extended_global r
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env lvar us args =
   match intern_extended_global_of_qualid (loc,qid) with
-  | TrueGlobal ref -> (Loc.tag ~loc @@ GRef (ref, us)), true, args
+  | TrueGlobal ref -> (Loc.tag ?loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
-      if List.length args < nids then error_not_enough_arguments ~loc;
+      if List.length args < nids then error_not_enough_arguments ?loc;
       let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
       let terms = make_subst ids (List.map fst args1) in
@@ -854,11 +856,11 @@ let intern_qualid loc qid intern env lvar us args =
       let c = instantiate_notation_constr loc intern lvar subst infos c in
       let c = match us, c with
       | None, _ -> c
-      | Some _, (loc, GRef (ref, None)) -> Loc.tag ~loc @@ GRef (ref, us)
+      | Some _, (loc, GRef (ref, None)) -> Loc.tag ?loc @@ GRef (ref, us)
       | Some _, (loc, GApp ((loc', GRef (ref, None)), arg)) ->
-        Loc.tag ~loc @@ GApp (Loc.tag ~loc:loc' @@ GRef (ref, us), arg)
+        Loc.tag ?loc @@ GApp (Loc.tag ?loc:loc' @@ GRef (ref, us), arg)
       | Some _, _ ->
-        user_err ~loc  (str "Notation " ++ pr_qualid qid ++
+        user_err ?loc  (str "Notation " ++ pr_qualid qid ++
           str " cannot have a universe instance, its expanded head
                does not start with a reference")
       in
@@ -874,7 +876,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
   | Qualid (loc, qid) ->
       let r,projapp,args2 =
 	try intern_qualid loc qid intern env ntnvars us args
-	with Not_found -> error_global_not_found ~loc qid
+	with Not_found -> error_global_not_found ?loc qid
       in
       let x, imp, scopes, l = find_appl_head_data r in
 	(x,imp,scopes,l), args2
@@ -890,7 +892,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
 	  (gvar (loc,id) us, [], [], []), args
-	else error_global_not_found ~loc qid
+	else error_global_not_found ?loc qid
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
@@ -952,7 +954,7 @@ let rec has_duplicate = function
   | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs =
- Loc.merge (fst (List.hd lhs)) (fst (List.last lhs))
+ Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -968,7 +970,7 @@ let check_number_of_pattern loc n l =
 
 let check_or_pat_variables loc ids idsl =
   if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then
-    user_err ~loc  (str
+    user_err ?loc  (str
     "The components of this disjunctive pattern must bind the same variables.")
 
 (** Use only when params were NOT asked to the user.
@@ -977,7 +979,7 @@ let check_constructor_length env loc cstr len_pl pl0 =
   let n = len_pl + List.length pl0 in
   if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
     (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
-      (error_wrong_numarg_constructor ~loc env cstr
+      (error_wrong_numarg_constructor ?loc env cstr
          (Inductiveops.constructor_nrealargs cstr)))
 
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
@@ -1002,14 +1004,14 @@ let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
   let nargs = Inductiveops.constructor_nallargs c in
   let nargs' = Inductiveops.constructor_nalldecls c in
   let impls_st = implicits_of_global (ConstructRef c) in
-  add_implicits_check_length (error_wrong_numarg_constructor ~loc env c)
+  add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
   let nallargs = inductive_nallargs_env env c in
   let nalldecls = inductive_nalldecls_env env c in
   let impls_st = implicits_of_global (IndRef c) in
-  add_implicits_check_length (error_wrong_numarg_inductive ~loc env c)
+  add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
     nallargs nalldecls impls_st len_pl1 pl2
 
 (** Do not raise NotEnoughArguments thanks to preconditions*)
@@ -1020,7 +1022,7 @@ let chop_params_pattern loc ind args with_letin =
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
   List.iter (function _, PatVar Anonymous -> ()
-    | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
+    | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:loc') params;
   args
 
 let find_constructor loc add_params ref =
@@ -1028,10 +1030,10 @@ let find_constructor loc add_params ref =
   | ConstructRef cstr -> cstr
   | IndRef _ ->
     let error = str "There is an inductive name deep in a \"in\" clause." in
-    user_err ~loc ~hdr:"find_constructor" error
+    user_err ?loc ~hdr:"find_constructor" error
   | ConstRef _ | VarRef _ ->
     let error = str "This reference is not a constructor." in
-    user_err ~loc ~hdr:"find_constructor" error
+    user_err ?loc ~hdr:"find_constructor" error
   in
   cstr, match add_params with
     | Some nb_args ->
@@ -1053,7 +1055,7 @@ let check_duplicate loc fields =
   match dups with
   | [] -> ()
   | (r, _) :: _ ->
-    user_err ~loc (str "This record defines several times the field " ++
+    user_err ?loc (str "This record defines several times the field " ++
       pr_reference r ++ str ".")
 
 (** [sort_fields ~complete loc fields completer] expects a list
@@ -1078,7 +1080,7 @@ let sort_fields ~complete loc fields completer =
             let gr = global_reference_of_reference first_field_ref in
             (gr, Recordops.find_projection gr)
           with Not_found ->
-            user_err ~loc:(loc_of_reference first_field_ref) ~hdr:"intern"
+            user_err ?loc:(loc_of_reference first_field_ref) ~hdr:"intern"
                          (pr_reference first_field_ref ++ str": Not a projection")
         in
         (* the number of parameters *)
@@ -1109,7 +1111,7 @@ let sort_fields ~complete loc fields completer =
                            by a let-in in the record declaration
                            (its value is fixed from other fields). *)
                        if first_field && not regular && complete then
-                         user_err ~loc  (str "No local fields allowed in a record construction.")
+                         user_err ?loc  (str "No local fields allowed in a record construction.")
                        else if first_field then
                          build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
                        else if not regular && complete then
@@ -1122,7 +1124,7 @@ let sort_fields ~complete loc fields completer =
               | None :: projs ->
                  if complete then
                    (* we don't want anonymous fields *)
-                   user_err ~loc  (str "This record contains anonymous fields.")
+                   user_err ?loc  (str "This record contains anonymous fields.")
                  else
                    (* anonymous arguments don't appear in proj_kinds *)
                    build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
@@ -1136,13 +1138,13 @@ let sort_fields ~complete loc fields completer =
             | (field_ref, field_value) :: fields ->
                let field_glob_ref = try global_reference_of_reference field_ref
                with Not_found ->
-                 user_err ~loc:(loc_of_reference field_ref) ~hdr:"intern"
+                 user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
                  let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
-                   user_err ~loc 
+                   user_err ?loc 
                      (str "This record contains fields of different records.")
                in
                index_fields fields remaining_projs ((field_index, field_value) :: acc)
@@ -1199,12 +1201,12 @@ let alias_of als = match als.alias_ids with
 
 let rec subst_pat_iterator y t (loc, p) = match p with
   | RCPatAtom id ->
-    begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ~loc p end
+    begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ?loc p end
   | RCPatCstr (id,l1,l2) ->
-     Loc.tag ~loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
+     Loc.tag ?loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
                                     List.map (subst_pat_iterator y t) l2)
-  | RCPatAlias (p,a) -> Loc.tag ~loc @@ RCPatAlias (subst_pat_iterator y t p,a)
-  | RCPatOr pl       -> Loc.tag ~loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
+  | RCPatAlias (p,a) -> Loc.tag ?loc @@ RCPatAlias (subst_pat_iterator y t p,a)
+  | RCPatOr pl       -> Loc.tag ?loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
 
 let drop_notations_pattern looked_for =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1214,7 +1216,7 @@ let drop_notations_pattern looked_for =
       if top then looked_for g else
       match g with ConstructRef _ -> () | _ -> raise Not_found
     with Not_found ->
-      error_invalid_pattern_notation ~loc ()
+      error_invalid_pattern_notation ?loc ()
   in
   let test_kind top =
     if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
@@ -1240,7 +1242,7 @@ let drop_notations_pattern looked_for =
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	      test_kind top g;
 	      let nvars = List.length vars in
-	      if List.length pats < nvars then error_not_enough_arguments ~loc;
+	      if List.length pats < nvars then error_not_enough_arguments ?loc;
 	      let pats1,pats2 = List.chop nvars pats in
 	      let subst = make_subst vars pats1 in
 	      let idspl1 = List.map (in_not false loc scopes (subst, Id.Map.empty) []) args in
@@ -1249,17 +1251,17 @@ let drop_notations_pattern looked_for =
 	| _ -> raise Not_found)
       | TrueGlobal g ->
 	  test_kind top g;
-	  Dumpglob.add_glob loc g;
+	  Dumpglob.add_glob ?loc g;
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
     with Not_found -> None
   and in_pat top scopes (loc, pt) = match pt with
-    | CPatAlias (p, id) -> Loc.tag ~loc @@ RCPatAlias (in_pat top scopes p, id)
+    | CPatAlias (p, id) -> Loc.tag ?loc @@ RCPatAlias (in_pat top scopes p, id)
     | CPatRecord l ->
       let sorted_fields =
 	sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in
       begin match sorted_fields with
-	| None -> Loc.tag ~loc @@ RCPatAtom None
+	| None -> Loc.tag ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
             if !asymmetric_patterns then pl else
@@ -1272,7 +1274,7 @@ let drop_notations_pattern looked_for =
     | CPatCstr (head, None, pl) ->
       begin
 	match drop_syndef top scopes head pl with
-	  | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr(a, b, c)
+	  | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr(a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
      | CPatCstr (r, Some expl_pl, pl) ->
@@ -1281,36 +1283,36 @@ let drop_notations_pattern looked_for =
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
-        Loc.tag ~loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+        Loc.tag ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
       else
         (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
-        Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+        Loc.tag ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
-      fst (Notation.interp_prim_token_cases_pattern_expr ~loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+      fst (Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (ntn, fullargs,extrargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
-      let ((ids',c),df) = Notation.interp_notation ~loc ntn scopes in
+      let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
       let (ids',idsl',_) = split_by_type ids' in
-      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
+      Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df;
       let substlist = make_subst idsl' argsl in
       let subst = make_subst ids' args in
       in_not top loc scopes (subst,substlist) extrargs c
     | CPatDelimiters (key, e) ->
-      in_pat top (None,find_delimiters_scope ~loc key::snd scopes) e
-    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ~loc (test_kind false) p scopes)
+      in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e
+    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes)
     | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
-	  | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr (a, b, c)
-	  | None         -> Loc.tag ~loc @@ RCPatAtom (Some (find_pattern_variable id))
+	  | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr (a, b, c)
+	  | None         -> Loc.tag ?loc @@ RCPatAtom (Some (find_pattern_variable id))
       end
-    | CPatAtom None -> Loc.tag ~loc @@ RCPatAtom None
-    | CPatOr pl     -> Loc.tag ~loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+    | CPatAtom None -> Loc.tag ?loc @@ RCPatAtom None
+    | CPatOr pl     -> Loc.tag ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
     | CPatCast _ ->
       assert false
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
@@ -1324,21 +1326,21 @@ let drop_notations_pattern looked_for =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-	  if Id.equal id ldots_var then Loc.tag ~loc @@ RCPatAtom (Some id) else
+	  if Id.equal id ldots_var then Loc.tag ?loc @@ RCPatAtom (Some id) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
       end
     | NRef g ->
       ensure_kind top loc g;
       let (_,argscs) = find_remaining_scopes [] args g in
-      Loc.tag ~loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
+      Loc.tag ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      Loc.tag ~loc @@ RCPatCstr (g,
+      Loc.tag ?loc @@ RCPatCstr (g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
-      if not (List.is_empty args) then user_err ~loc 
+      if not (List.is_empty args) then user_err ?loc 
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
          (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -1353,8 +1355,8 @@ let drop_notations_pattern looked_for =
          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole _ ->
       let () = assert (List.is_empty args) in
-      Loc.tag ~loc @@ RCPatAtom None
-    | t -> error_invalid_pattern_notation ~loc ()
+      Loc.tag ?loc @@ RCPatAtom None
+    | t -> error_invalid_pattern_notation ?loc ()
   in in_pat true
 
 let rec intern_pat genv aliases pat =
@@ -1362,7 +1364,7 @@ let rec intern_pat genv aliases pat =
     let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
     let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
-      (asubst, Loc.tag ~loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+      (asubst, Loc.tag ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
   match pat with
     | loc, RCPatAlias (p, id) ->
@@ -1382,10 +1384,10 @@ let rec intern_pat genv aliases pat =
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
     | loc, RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
-      (aliases.alias_ids,[aliases.alias_map, Loc.tag ~loc @@ PatVar (alias_of aliases)])
+      (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)])
     | loc, RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
-      (ids, [asubst, Loc.tag ~loc @@ PatVar (alias_of aliases)])
+      (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)])
     | loc, RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
@@ -1406,7 +1408,7 @@ let rec intern_pat genv aliases pat =
    [pattern] rule. *)
 let rec check_no_patcast (loc, pt) = match pt with
   | CPatCast (_,_) ->
-     CErrors.user_err ~loc ~hdr:"check_no_patcast"
+     CErrors.user_err ?loc ~hdr:"check_no_patcast"
                            (Pp.strbrk "Casts are not supported here.")
   | CPatDelimiters(_,p)
   | CPatAlias(p,_) -> check_no_patcast p
@@ -1440,11 +1442,11 @@ let intern_ind_pattern genv scopes pat =
   let no_not =
     try
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
-    with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc
+    with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
   in
   match no_not with
     | loc, RCPatCstr (head, expl_pl, pl) ->
-      let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in
+      let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
       let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
@@ -1452,8 +1454,8 @@ let intern_ind_pattern genv scopes pat =
       (with_letin,
        match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
        | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
-       | _ -> error_bad_inductive_type ~loc)
-    | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x)
+       | _ -> error_bad_inductive_type ?loc)
+    | x -> error_bad_inductive_type ?loc:(raw_cases_pattern_expr_loc x)
 
 (**********************************************************************)
 (* Utilities for application                                          *)
@@ -1474,8 +1476,8 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
-  | (loc, GVar id) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+  | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+  | (loc, GVar id) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
@@ -1492,10 +1494,10 @@ let extract_explicit_arg imps args =
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
-		user_err ~loc 
+		user_err ?loc 
 		  (str "Wrong argument name: " ++ pr_id id ++ str ".");
 	      if Id.Map.mem id eargs then
-		user_err ~loc  (str "Argument name " ++ pr_id id
+		user_err ?loc  (str "Argument name " ++ pr_id id
 		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
@@ -1505,11 +1507,11 @@ let extract_explicit_arg imps args =
 		  if not (is_status_implicit imp) then failwith "imp";
 		  name_of_implicit imp
 		with Failure _ (* "nth" | "imp" *) ->
-		  user_err ~loc 
+		  user_err ?loc 
 		    (str"Wrong argument position: " ++ int p ++ str ".")
 	      in
 	      if Id.Map.mem id eargs then
-		user_err ~loc  (str"Argument at position " ++ int p ++
+		user_err ?loc  (str"Argument at position " ++ int p ++
 		  str " is mentioned more than once.");
 	      id in
 	  (Id.Map.add id (loc, a) eargs, rargs)
@@ -1519,7 +1521,7 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
-  let rec intern env = Loc.with_loc (fun ~loc -> function
+  let rec intern env = Loc.with_loc (fun ?loc -> function
     | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env (Environ.named_context globalenv)
@@ -1564,7 +1566,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
 					    en (Loc.tag @@ Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
           GRec (GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
@@ -1591,7 +1593,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
 					    en (Loc.tag @@ Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GRec (GCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
@@ -1600,30 +1602,30 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CProdN ([],c2) ->
         intern_type env c2
     | CProdN ((nal,bk,ty)::bll,c2) ->
-        iterate_prod loc env bk ty (Loc.tag ~loc @@ CProdN (bll, c2)) nal
+        iterate_prod ?loc env bk ty (Loc.tag ?loc @@ CProdN (bll, c2)) nal
     | CLambdaN ([],c2) ->
         intern env c2
     | CLambdaN ((nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ~loc @@ CLambdaN (bll, c2)) nal
+	iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ?loc @@ CLambdaN (bll, c2)) nal
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
-	intern env (Loc.tag ~loc @@ CPrim (Numeral (Bigint.neg p)))
+	intern env (Loc.tag ?loc @@ CPrim (Numeral (Bigint.neg p)))
     | CNotation ("( _ )",([a],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
     | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
     | CPrim p ->
-	fst (Notation.interp_prim_token ~loc p (env.tmp_scope,env.scopes))
+	fst (Notation.interp_prim_token ?loc p (env.tmp_scope,env.scopes))
     | CDelimiters (key, e) ->
 	intern {env with tmp_scope = None;
-		  scopes = find_delimiters_scope ~loc key :: env.scopes} e
+		  scopes = find_delimiters_scope ?loc key :: env.scopes} e
     | CAppExpl ((isproj,ref,us), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
@@ -1631,7 +1633,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    lvar us args ref 
 	in
 	  (* Rem: GApp(_,f,[]) stands for @f *)
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	  GApp (f, intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
@@ -1658,15 +1660,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> Loc.tag ~loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+	             (fun _idx -> Loc.tag ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
                                                          Misctypes.IntroAnonymous, None))
        in
        begin
 	  match fields with
-	    | None -> user_err ~loc ~hdr:"intern" (str"No constructor inference.")
+	    | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
-                let app = Loc.tag ~loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
+		let pars = List.make n (Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+                let app = Loc.tag ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
 	  intern env app
 	end
     | CCases (sty, rtnpo, tms, eqns) ->
@@ -1701,7 +1703,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
              let main_sub_eqn = Loc.tag @@
                ([],thepats, (* "|p1,..,pn" *)
 		Option.cata (intern_type env')
-                  (Loc.tag ~loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+                  (Loc.tag ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
@@ -1710,7 +1712,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
              Some (Loc.tag @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GCases (sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
@@ -1720,7 +1722,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.tag na') in
 	  intern_type env'' u) po in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
         GLetTuple (List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (c, (na,po), b1, b2) ->
@@ -1730,7 +1732,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.tag na') in
 	  intern_type env'' p) po in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
         GIf (c', (na', p'), intern env b1, intern env b2)
     | CHole (k, naming, solve) ->
         let k = match k with
@@ -1756,28 +1758,28 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
         in
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GHole (k, naming, solve)
     (* Parsing pattern variables *)
     | CPatVar n when allow_patvar ->
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GPatVar (true,n)
     | CEvar (n, []) when allow_patvar ->
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GPatVar (false,n)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (n, l) ->
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GEvar (n, List.map (on_snd (intern env)) l)
     | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
     | CSort s ->
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
 	GSort s
     | CCast (c1, c2) ->
-	Loc.tag ~loc @@
+	Loc.tag ?loc @@
         GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
   )
   and intern_type env = intern (set_type_scope env)
@@ -1836,7 +1838,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
 	    let add_name l = function
 	      | _,Anonymous -> l
-	      | loc,(Name y as x) -> (y, Loc.tag ~loc @@ PatVar x) :: l in
+	      | loc,(Name y as x) -> (y, Loc.tag ?loc @@ PatVar x) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
@@ -1860,13 +1862,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
       [], None in
     (tm',(snd na,typ)), extra_id, match_td
 
-  and iterate_prod loc2 env bk ty body nal =
+  and iterate_prod ?loc env bk ty body nal =
     let env, bl = intern_assumption intern ntnvars env nal bk ty in
-    it_mkGProd loc2 bl (intern_type env body)
+    it_mkGProd ?loc bl (intern_type env body)
 
-  and iterate_lam loc2 env bk ty body nal =
+  and iterate_lam loc env bk ty body nal =
     let env, bl = intern_assumption intern ntnvars env nal bk ty in
-    it_mkGLambda loc2 bl (intern env body)
+    it_mkGLambda ?loc bl (intern env body)
 
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
@@ -1898,7 +1900,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
       | (imp::impl', []) ->
 	  if not (Id.Map.is_empty eargs) then
 	    (let (id,(loc,_)) = Id.Map.choose eargs in
-	       user_err ~loc  (str "Not enough non implicit \
+	       user_err ?loc  (str "Not enough non implicit \
 	    arguments to accept the argument bound to " ++
 		 pr_id id ++ str"."));
 	  []
@@ -1915,8 +1917,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   and smart_gapp f loc = function
     | [] -> f
     | l -> match f with
-      | (loc', GApp (g, args)) -> Loc.tag ~loc:(Loc.merge loc' loc) @@ GApp (g, args@l)
-      | _ -> Loc.tag ~loc:(Loc.merge (loc_of_glob_constr f) loc) @@ GApp (f, l)
+      | (loc', GApp (g, args)) -> Loc.tag ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l)
+      | _ -> Loc.tag ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l)
 
   and intern_args env subscopes = function
     | [] -> []
@@ -1929,7 +1931,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     intern env c
   with
       InternalizationError (loc,e) ->
-	user_err ~loc ~hdr:"internalize"
+	user_err ?loc ~hdr:"internalize"
 	  (explain_internalization_error e)
 
 (**************************************************************************)
@@ -1969,7 +1971,7 @@ let intern_pattern globalenv patt =
     intern_cases_pattern globalenv (None,[]) empty_alias patt
   with
       InternalizationError (loc,e) ->
-	user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
+	user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
 
 (*********************************************************************)
@@ -2055,12 +2057,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
 
 let interp_binder env sigma na t =
   let t = intern_gen IsType env t in
-  let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
+  let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
   understand ~expected_type:IsType env sigma t'
 
 let interp_binder_evars env evdref na t =
   let t = intern_gen IsType env t in
-  let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
+  let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
   understand_tcc_evars env evdref ~expected_type:IsType t'
 
 open Environ
@@ -2079,7 +2081,7 @@ let intern_context global_level env impl_env binders =
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map glob_local_binder_of_extended bl)
   with InternalizationError (loc,e) ->
-    user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
+    user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
 let interp_rawcontext_evars env evdref k bl =
   let open EConstr in
@@ -2087,7 +2089,7 @@ let interp_rawcontext_evars env evdref k bl =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
        let t' =
-	 if Option.is_empty b then locate_if_hole ~loc:(loc_of_glob_constr t) na t
+	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
        let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
-- 
cgit v1.2.3


From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 8 Apr 2017 23:19:35 +0200
Subject: [location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.
---
 interp/constrintern.ml | 133 ++++++++++++++++++++++++++-----------------------
 1 file changed, 70 insertions(+), 63 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a672771b14..541b529729 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -217,7 +217,7 @@ let contract_notation ntn (l,ll,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | (_loc, CNotation ("{ _ }",([a],[],[]))) :: l ->
+    | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -230,7 +230,7 @@ let contract_pat_notation ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | (_, CPatNotation ("{ _ }",([a],[]),[])) :: l ->
+    | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -407,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	  let name =
 	    let id =
 	      match ty with
-	      | _, CApp ((_, (_, CRef (Ident (loc,id),_))), _) -> id
+	      | { CAst.v = CApp ((_, { CAst.v = CRef (Ident (loc,id),_) } ), _) } -> id
 	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
@@ -430,7 +430,7 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
-let rec free_vars_of_pat il (loc, pt) = match pt with
+let rec free_vars_of_pat il pt = match CAst.(pt.v) with
   | CPatCstr (c, l1, l2) ->
       let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
       List.fold_left free_vars_of_pat il l2
@@ -448,7 +448,7 @@ let intern_local_pattern intern lvar env p =
   List.fold_left
     (fun env (loc, i) ->
        let bk = Default Implicit in
-       let ty = Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
+       let ty = CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
        let n = Name i in
        let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
        env)
@@ -480,7 +480,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let tyc =
         match ty with
         | Some ty -> ty
-        | None -> Loc.tag ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+        | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
       let il = List.map snd (free_vars_of_pat [] p) in
@@ -596,16 +596,16 @@ let rec subordinate_letins letins = function
       letins,[]
 
 let terms_of_binders bl =
-  let rec term_of_pat pt = Loc.map_with_loc (fun ?loc -> function
+  let rec term_of_pat pt = CAst.map_from_loc (fun ?loc -> function
     | PatVar (Name id)   -> CRef (Ident (loc,id), None)
     | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
     | PatCstr (c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
-       let hole = Loc.tag ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+       let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
-    | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+    | (loc, GLocalAssum (Name id,_,_))::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
     | (loc, GLocalDef (Anonymous,_,_,_))::l
     | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
@@ -760,7 +760,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
     let expl_impls = List.map
-      (fun id -> Loc.tag ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+      (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -993,10 +993,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,(Loc.tag @@ RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom(None))::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,(Loc.tag @@ RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1199,14 +1199,15 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let rec subst_pat_iterator y t (loc, p) = match p with
-  | RCPatAtom id ->
-    begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ?loc p end
+let rec subst_pat_iterator y t = CAst.map (function
+  | RCPatAtom id as p ->
+    begin match id with Some x when Id.equal x y -> t.CAst.v | _ -> p end
   | RCPatCstr (id,l1,l2) ->
-     Loc.tag ?loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
-                                    List.map (subst_pat_iterator y t) l2)
-  | RCPatAlias (p,a) -> Loc.tag ?loc @@ RCPatAlias (subst_pat_iterator y t p,a)
-  | RCPatOr pl       -> Loc.tag ?loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
+    RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
+                   List.map (subst_pat_iterator y t) l2)
+  | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
+  | RCPatOr pl       -> RCPatOr (List.map (subst_pat_iterator y t) pl)
+  )
 
 let drop_notations_pattern looked_for =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1255,26 +1256,29 @@ let drop_notations_pattern looked_for =
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
     with Not_found -> None
-  and in_pat top scopes (loc, pt) = match pt with
-    | CPatAlias (p, id) -> Loc.tag ?loc @@ RCPatAlias (in_pat top scopes p, id)
+  and in_pat top scopes pt =
+    let open CAst in
+    let loc = pt.loc in
+    match pt.v with
+    | CPatAlias (p, id) -> CAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
     | CPatRecord l ->
       let sorted_fields =
-	sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in
+	sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
       begin match sorted_fields with
-	| None -> Loc.tag ?loc @@ RCPatAtom None
+	| None -> CAst.make ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
             if !asymmetric_patterns then pl else
-            let pars = List.make n (loc, CPatAtom None) in
+            let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
             List.rev_append pars pl in
 	  match drop_syndef top scopes head pl with
-	    |Some (a,b,c) -> (loc, RCPatCstr(a, b, c))
-	    |None -> raise (InternalizationError (loc,NotAConstructor head))
+	    | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
+	    | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
     | CPatCstr (head, None, pl) ->
       begin
 	match drop_syndef top scopes head pl with
-	  | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr(a, b, c)
+	  | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
      | CPatCstr (r, Some expl_pl, pl) ->
@@ -1283,13 +1287,13 @@ let drop_notations_pattern looked_for =
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
-        Loc.tag ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+        CAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
       else
         (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
-        Loc.tag ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
+        CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
 	when Bigint.is_strictly_pos p ->
       fst (Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
     | CPatNotation ("( _ )",([a],[]),[]) ->
@@ -1308,11 +1312,11 @@ let drop_notations_pattern looked_for =
     | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
-	  | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr (a, b, c)
-	  | None         -> Loc.tag ?loc @@ RCPatAtom (Some (find_pattern_variable id))
+	  | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr (a, b, c)
+	  | None         -> CAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id))
       end
-    | CPatAtom None -> Loc.tag ?loc @@ RCPatAtom None
-    | CPatOr pl     -> Loc.tag ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+    | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None
+    | CPatOr pl     -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
     | CPatCast _ ->
       assert false
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
@@ -1326,17 +1330,17 @@ let drop_notations_pattern looked_for =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-	  if Id.equal id ldots_var then Loc.tag ?loc @@ RCPatAtom (Some id) else
+	  if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
       end
     | NRef g ->
       ensure_kind top loc g;
       let (_,argscs) = find_remaining_scopes [] args g in
-      Loc.tag ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
+      CAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      Loc.tag ?loc @@ RCPatCstr (g,
+      CAst.make ?loc @@ RCPatCstr (g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
@@ -1355,7 +1359,7 @@ let drop_notations_pattern looked_for =
          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole _ ->
       let () = assert (List.is_empty args) in
-      Loc.tag ?loc @@ RCPatAtom None
+      CAst.make ?loc @@ RCPatAtom None
     | t -> error_invalid_pattern_notation ?loc ()
   in in_pat true
 
@@ -1366,11 +1370,12 @@ let rec intern_pat genv aliases pat =
     let pl' = List.map (fun (asubst,pl) ->
       (asubst, Loc.tag ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
-  match pat with
-    | loc, RCPatAlias (p, id) ->
+  let loc = CAst.(pat.loc) in
+  match CAst.(pat.v) with
+    | RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_pat genv aliases' p
-    | loc, RCPatCstr (head, expl_pl, pl) ->
+    | RCPatCstr (head, expl_pl, pl) ->
       if !asymmetric_patterns then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
@@ -1382,13 +1387,13 @@ let rec intern_pat genv aliases pat =
 	let with_letin, pl2 =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
-    | loc, RCPatAtom (Some id) ->
+    | RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
       (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)])
-    | loc, RCPatAtom (None) ->
+    | RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
       (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)])
-    | loc, RCPatOr pl ->
+    | RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
       let (idsl,pl') = List.split pl' in
@@ -1406,9 +1411,9 @@ let rec intern_pat genv aliases pat =
    of lambdas in the encoding of match in constr. We put this check here and not
    in the parser because it would require to duplicate the levels of the
    [pattern] rule. *)
-let rec check_no_patcast (loc, pt) = match pt with
+let rec check_no_patcast pt = match CAst.(pt.v) with
   | CPatCast (_,_) ->
-     CErrors.user_err ?loc ~hdr:"check_no_patcast"
+     CErrors.user_err ?loc:pt.CAst.loc ~hdr:"check_no_patcast"
                            (Pp.strbrk "Casts are not supported here.")
   | CPatDelimiters(_,p)
   | CPatAlias(p,_) -> check_no_patcast p
@@ -1444,8 +1449,9 @@ let intern_ind_pattern genv scopes pat =
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
   in
-  match no_not with
-    | loc, RCPatCstr (head, expl_pl, pl) ->
+  let loc = no_not.CAst.loc in
+  match no_not.CAst.v with
+    | RCPatCstr (head, expl_pl, pl) ->
       let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
@@ -1455,7 +1461,7 @@ let intern_ind_pattern genv scopes pat =
        match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
        | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
        | _ -> error_bad_inductive_type ?loc)
-    | x -> error_bad_inductive_type ?loc:(raw_cases_pattern_expr_loc x)
+    | x -> error_bad_inductive_type ?loc
 
 (**********************************************************************)
 (* Utilities for application                                          *)
@@ -1521,7 +1527,7 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
-  let rec intern env = Loc.with_loc (fun ?loc -> function
+  let rec intern env = CAst.with_loc_val (fun ?loc -> function
     | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env (Environ.named_context globalenv)
@@ -1602,20 +1608,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CProdN ([],c2) ->
         intern_type env c2
     | CProdN ((nal,bk,ty)::bll,c2) ->
-        iterate_prod ?loc env bk ty (Loc.tag ?loc @@ CProdN (bll, c2)) nal
+        iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal
     | CLambdaN ([],c2) ->
         intern env c2
     | CLambdaN ((nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ?loc @@ CLambdaN (bll, c2)) nal
+	iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?loc @@ CLambdaN (bll, c2)) nal
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
 	Loc.tag ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
+    | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
 	when Bigint.is_strictly_pos p ->
-	intern env (Loc.tag ?loc @@ CPrim (Numeral (Bigint.neg p)))
+	intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p)))
     | CNotation ("( _ )",([a],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
@@ -1639,20 +1645,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CApp ((isproj,f), args) ->
         let f,args = match f with
           (* Compact notations like "t.(f args') args" *)
-          | _loc, CApp ((Some _,f), args') when not (Option.has_some isproj) ->
+          | { CAst.v = CApp ((Some _,f), args') } when not (Option.has_some isproj) ->
 	    f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
           | _ -> f,args in
 	let (c,impargs,args_scopes,l),args =
-          match f with
-            | _loc, CRef (ref,us) -> 
+          match f.CAst.v with
+            | CRef (ref,us) -> 
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
-            | _loc, CNotation (ntn,([],[],[])) ->
+            | CNotation (ntn,([],[],[])) ->
                 let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
-            | x -> (intern env f,[],[],[]), args in
+            | _ -> (intern env f,[],[],[]), args in
           apply_impargs c env impargs args_scopes
 	    (merge_impargs l args) loc
 
@@ -1660,15 +1666,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> Loc.tag ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
-                                                         Misctypes.IntroAnonymous, None))
+	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+                                                           Misctypes.IntroAnonymous, None))
        in
        begin
 	  match fields with
 	    | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
-                let app = Loc.tag ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
+		let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+                let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
 	  intern env app
 	end
     | CCases (sty, rtnpo, tms, eqns) ->
@@ -1910,6 +1916,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     in aux 1 l subscopes eargs rargs
 
   and apply_impargs c env imp subscopes l loc =
+    let l : (Constrexpr.constr_expr * Constrexpr.explicitation Loc.located option) list = l in
     let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
     let l = intern_impargs c env imp subscopes l in
       smart_gapp c loc l
-- 
cgit v1.2.3


From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Apr 2017 03:35:20 +0200
Subject: [location] [ast] Port module AST to CAst

---
 interp/constrintern.ml | 167 +++++++++++++++++++++++++------------------------
 1 file changed, 84 insertions(+), 83 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 541b529729..bd7c05e6f8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -15,6 +15,7 @@ open Namegen
 open Libnames
 open Globnames
 open Impargs
+open CAst
 open Glob_term
 open Glob_ops
 open Patternops
@@ -304,12 +305,12 @@ let reset_tmp_scope env = {env with tmp_scope = None}
 
 let rec it_mkGProd ?loc env body =
   match env with
-      (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
+      (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
     | [] -> body
 
 let rec it_mkGLambda ?loc env body =
   match env with
-      (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
+      (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -322,14 +323,14 @@ let build_impls = function
 
 let impls_type_list ?(args = []) =
   let rec aux acc = function
-    |_, GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
-    |_ -> (Variable,[],List.append args (List.rev acc),[])
+    | { v = GProd (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c
+    | _ -> (Variable,[],List.append args (List.rev acc),[])
   in aux []
 
 let impls_term_list ?(args = []) =
   let rec aux acc = function
-    |_, GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
-    |_, GRec (fix_kind, nas, args, tys, bds) ->
+    | { v = GLambda (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c
+    | { v = GRec (fix_kind, nas, args, tys, bds) } ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
 	 aux acc' bds.(nb)
@@ -346,12 +347,12 @@ let rec check_capture ty = function
       ()
 
 let locate_if_hole ?loc na = function
-  | _, GHole (_,naming,arg) ->
+  | { v = GHole (_,naming,arg) } ->
       (try match na with
 	| Name id -> glob_constr_of_notation_constr ?loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
+      with Not_found -> CAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -397,7 +398,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
     env fvs in
   let bl = List.map
     (fun (loc, id) ->
-      (loc, (Name id, b, Loc.tag ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+      (loc, (Name id, b, CAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -454,11 +455,11 @@ let intern_local_pattern intern lvar env p =
        env)
     env (free_vars_of_pat [] p)
 
-let glob_local_binder_of_extended = Loc.with_loc (fun ?loc -> function
+let glob_local_binder_of_extended = CAst.with_loc_val (fun ?loc -> function
   | GLocalAssum (na,bk,t) -> (na,bk,None,t)
   | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
   | GLocalDef (na,bk,c,None) ->
-      let t = Loc.tag ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+      let t = CAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
       (na,bk,Some c,t)
   | GLocalPattern (_,_,_,_) ->
       Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
@@ -469,13 +470,13 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd"
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
-      let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ?loc @@ GLocalAssum (na,c,t)) bl' in
+      let bl' = List.map (fun (loc,(na,c,t)) -> CAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
       env, bl' @ bl
   | CLocalDef((loc,na as locna),def,ty) ->
      let term = intern env def in
      let ty = Option.map (intern env) ty in
       (push_name_env lvar (impls_term_list term) env locna,
-       (Loc.tag ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
+       (CAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
   | CLocalPattern (loc,(p,ty)) ->
       let tyc =
         match ty with
@@ -495,7 +496,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
       let _,(_,bk,t) = List.hd bl' in
-      (env, (Loc.tag ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
+      (env, (CAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -518,12 +519,12 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (loc', id) acc ->
-            Loc.tag ?loc:(Loc.merge_opt loc' loc) @@
-	    GProd (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            CAst.make ?loc:(Loc.merge_opt loc' loc) @@
+	    GProd (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
 	else
 	  (fun (loc', id) acc ->
-            Loc.tag ?loc:(Loc.merge_opt loc' loc) @@
-	    GLambda (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            CAst.make ?loc:(Loc.merge_opt loc' loc) @@
+	    GLambda (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
     in
       List.fold_right (fun (loc, id as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -576,27 +577,27 @@ let make_letins =
     (fun a c ->
      match a with
      | loc, LPLetIn (na,b,t) ->
-       Loc.tag ?loc @@ GLetIn(na,b,t,c)
+       CAst.make ?loc @@ GLetIn(na,b,t,c)
      | loc, LPCases ((cp,il),id) ->
-         let tt = (Loc.tag ?loc @@ GVar id, (Name id,None)) in
-         Loc.tag ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
+         let tt = (CAst.make ?loc @@ GVar id, (Name id,None)) in
+         CAst.make ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
 
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
-  | (loc, GLocalDef (na,_,b,t))::l ->
+  | { loc; v = GLocalDef (na,_,b,t) }::l ->
       subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l
-  | (loc, GLocalAssum (na,bk,t))::l ->
+  | { loc; v = GLocalAssum (na,bk,t)}::l ->
       let letins',rest = subordinate_letins [] l in
       letins',((loc,(na,bk,t)),letins)::rest
-  | (loc, GLocalPattern (u,id,bk,t)) :: l ->
+  | { loc; v = GLocalPattern (u,id,bk,t)} :: l ->
       subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins)
-                          ([Loc.tag ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
+                          ([CAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
   | [] ->
       letins,[]
 
 let terms_of_binders bl =
-  let rec term_of_pat pt = CAst.map_from_loc (fun ?loc -> function
+  let rec term_of_pat pt = CAst.map_with_loc (fun ?loc -> function
     | PatVar (Name id)   -> CRef (Ident (loc,id), None)
     | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
     | PatCstr (c,l,_) ->
@@ -605,11 +606,11 @@ let terms_of_binders bl =
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
-    | (loc, GLocalAssum (Name id,_,_))::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
-    | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
-    | (loc, GLocalDef (Anonymous,_,_,_))::l
-    | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
-    | (loc, GLocalPattern ((u,_),_,_,_)) :: l -> term_of_pat u :: extract_variables l
+    | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+    | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l
+    | {loc; v = GLocalDef (Anonymous,_,_,_)}::l
+    | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> error "Cannot turn \"_\" into a term."
+    | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l
     | [] -> [] in
   extract_variables bl
 
@@ -665,7 +666,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let bindings = Id.Map.map mk_env terms in
         Some (Genintern.generic_substitute_notation bindings arg)
       in
-      Loc.tag ?loc @@ GHole (knd, naming, arg)
+      CAst.make ?loc @@ GHole (knd, naming, arg)
     | NBinderList (x,y,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -683,22 +684,22 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
         let (loc,(na,bk,t)) = a in
-        Loc.tag ?loc @@ GProd (na,bk,t,e)
+        CAst.make ?loc @@ GProd (na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let (loc,(na,bk,t)) = a in
-        Loc.tag ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
+        CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-	Loc.tag ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
+        let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	CAst.make ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
     | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-	Loc.tag ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
+        let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	CAst.make ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
     | t ->
       glob_constr_of_notation_constr_with_binders ?loc
         (traverse_binder subst avoid) (aux subst') subinfos t
@@ -710,7 +711,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       intern {env with tmp_scope = scopt;
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
-    Loc.tag ?loc (
+    CAst.make ?loc (
     try
       GVar (Id.Map.find id renaming)
     with Not_found ->
@@ -750,7 +751,7 @@ let string_of_ty = function
   | Variable -> "var"
 
 let gvar (loc, id) us = match us with
-| None -> Loc.tag ?loc @@ GVar id
+| None -> CAst.make ?loc @@ GVar id
 | Some _ ->
   user_err ?loc  (str "Variable " ++ pr_id id ++
     str " cannot have a universe instance")
@@ -792,18 +793,18 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	Loc.tag ?loc @@ GRef (ref, us), impls, scopes, []
+	CAst.make ?loc @@ GRef (ref, us), impls, scopes, []
       with e when CErrors.noncritical e ->
 	(* [id] a goal variable *)
 	gvar (loc,id) us, [], [], []
 
 let find_appl_head_data c =
-  match Loc.obj c with
+  match c.v with
   | GRef (ref,_) ->
     let impls = implicits_of_global ref in
     let scopes = find_arguments_scope ref in
       c, impls, scopes, []
-  | GApp ((_, GRef (ref,_)),l)
+  | GApp ({ v = GRef (ref,_) },l)
       when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       let impls = implicits_of_global ref in 
@@ -842,7 +843,7 @@ let intern_reference ref =
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env lvar us args =
   match intern_extended_global_of_qualid (loc,qid) with
-  | TrueGlobal ref -> (Loc.tag ?loc @@ GRef (ref, us)), true, args
+  | TrueGlobal ref -> (CAst.make ?loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
@@ -856,9 +857,9 @@ let intern_qualid loc qid intern env lvar us args =
       let c = instantiate_notation_constr loc intern lvar subst infos c in
       let c = match us, c with
       | None, _ -> c
-      | Some _, (loc, GRef (ref, None)) -> Loc.tag ?loc @@ GRef (ref, us)
-      | Some _, (loc, GApp ((loc', GRef (ref, None)), arg)) ->
-        Loc.tag ?loc @@ GApp (Loc.tag ?loc:loc' @@ GRef (ref, us), arg)
+      | Some _, { loc; v = GRef (ref, None) } -> CAst.make ?loc @@ GRef (ref, us)
+      | Some _, { loc; v = GApp ({ loc = loc' ; v = GRef (ref, None) }, arg) } ->
+        CAst.make ?loc @@ GApp (CAst.make ?loc:loc' @@ GRef (ref, us), arg)
       | Some _, _ ->
         user_err ?loc  (str "Notation " ++ pr_qualid qid ++
           str " cannot have a universe instance, its expanded head
@@ -869,7 +870,7 @@ let intern_qualid loc qid intern env lvar us args =
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar us args =
   match intern_qualid loc qid intern env lvar us args with
-    | (_, GRef (VarRef _, _)),_,_ -> raise Not_found
+    | { v = GRef (VarRef _, _) },_,_ -> raise Not_found
     | r -> r
 
 let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
@@ -1021,8 +1022,8 @@ let chop_params_pattern loc ind args with_letin =
     else Inductiveops.inductive_nparams ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
-  List.iter (function _, PatVar Anonymous -> ()
-    | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:loc') params;
+  List.iter (function { v = PatVar Anonymous } -> ()
+    | { loc; v = PatVar _ } | { loc; v = PatCstr(_,_,_) } -> error_parameter_not_implicit ?loc) params;
   args
 
 let find_constructor loc add_params ref =
@@ -1042,7 +1043,7 @@ let find_constructor loc add_params ref =
           then Inductiveops.inductive_nparamdecls ind
           else Inductiveops.inductive_nparams ind
       in
-      List.make nb ([], [(Id.Map.empty, Loc.tag @@ PatVar Anonymous)])
+      List.make nb ([], [(Id.Map.empty, CAst.make @@ PatVar Anonymous)])
     | None -> []
 
 let find_pattern_variable = function
@@ -1368,7 +1369,7 @@ let rec intern_pat genv aliases pat =
     let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
     let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
-      (asubst, Loc.tag ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+      (asubst, CAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
   let loc = CAst.(pat.loc) in
   match CAst.(pat.v) with
@@ -1389,10 +1390,10 @@ let rec intern_pat genv aliases pat =
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
     | RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
-      (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)])
+      (aliases.alias_ids,[aliases.alias_map, CAst.make ?loc @@ PatVar (alias_of aliases)])
     | RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
-      (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)])
+      (ids, [asubst, CAst.make ?loc @@ PatVar (alias_of aliases)])
     | RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
@@ -1482,8 +1483,8 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
-  | (loc, GVar id) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+  | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+  | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
@@ -1549,7 +1550,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       let before, after = split_at_annot bl n in
 	       let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
 	       let ro = f (intern env') in
-	       let n' = Option.map (fun _ -> List.count (function | _, GLocalAssum _ -> true
+	       let n' = Option.map (fun _ -> List.count (function | { v = GLocalAssum _ } -> true
                                                                   | _ -> false (* remove let-ins *))
                         rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
@@ -1572,7 +1573,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
 					    en (Loc.tag @@ Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
           GRec (GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
@@ -1599,7 +1600,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
 					    en (Loc.tag @@ Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GRec (GCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
@@ -1616,7 +1617,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
@@ -1639,7 +1640,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    lvar us args ref 
 	in
 	  (* Rem: GApp(_,f,[]) stands for @f *)
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	  GApp (f, intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
@@ -1696,7 +1697,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let stripped_match_from_in =
           let rec aux = function
 	    | [] -> []
-	    | (_, (_loc, PatVar _)) :: q -> aux q
+	    | (_, { v = PatVar _}) :: q -> aux q
 	    | l -> l
 	  in aux match_from_in in
         let rtnpo = match stripped_match_from_in with
@@ -1705,20 +1706,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
              (* Build a return predicate by expansion of the patterns of the "in" clause *)
              let thevars, thepats = List.split l in
              let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
-             let sub_tms = List.map (fun id -> (Loc.tag @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
+             let sub_tms = List.map (fun id -> (CAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
              let main_sub_eqn = Loc.tag @@
                ([],thepats, (* "|p1,..,pn" *)
 		Option.cata (intern_type env')
-                  (Loc.tag ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+                  (CAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
-                  [Loc.tag @@ ([],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
-                   Loc.tag @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
-             Some (Loc.tag @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+                  [Loc.tag @@ ([],List.make (List.length thepats) (CAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
+                   CAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
+             Some (CAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GCases (sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
@@ -1728,7 +1729,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.tag na') in
 	  intern_type env'' u) po in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
         GLetTuple (List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (c, (na,po), b1, b2) ->
@@ -1738,7 +1739,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.tag na') in
 	  intern_type env'' p) po in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
         GIf (c', (na', p'), intern env b1, intern env b2)
     | CHole (k, naming, solve) ->
         let k = match k with
@@ -1764,28 +1765,28 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
         in
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GHole (k, naming, solve)
     (* Parsing pattern variables *)
     | CPatVar n when allow_patvar ->
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GPatVar (true,n)
     | CEvar (n, []) when allow_patvar ->
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GPatVar (false,n)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (n, l) ->
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GEvar (n, List.map (on_snd (intern env)) l)
     | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
     | CSort s ->
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
 	GSort s
     | CCast (c1, c2) ->
-	Loc.tag ?loc @@
+	CAst.make ?loc @@
         GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
   )
   and intern_type env = intern (set_type_scope env)
@@ -1824,8 +1825,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     let tm' = intern env tm in
     (* the "as" part *)
     let extra_id,na = match tm', na with
-      | (loc , GVar id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
-      | (loc, GRef (VarRef id, _)), None -> Some id,(loc,Name id)
+      | {loc; v = GVar id}, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
+      | {loc; v = GRef (VarRef id, _)}, None -> Some id,(loc,Name id)
       | _, None -> None,(Loc.tag Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
     (* the "in" part *)
@@ -1844,14 +1845,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
 	    let add_name l = function
 	      | _,Anonymous -> l
-	      | loc,(Name y as x) -> (y, Loc.tag ?loc @@ PatVar x) :: l in
+	      | loc,(Name y as x) -> (y, CAst.make ?loc @@ PatVar x) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
 		canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc)
 	      | [],[] ->
 		(add_name match_acc na, var_acc)
-	      | _::t, (loc, PatVar x)::tt ->
+	      | _::t, { loc; v = PatVar x}::tt ->
 		canonize_args t tt forbidden_names
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
 	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
@@ -1897,7 +1898,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
             (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
-              (Loc.map (fun (a,b,c) -> GHole(a,b,c))
+              (CAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c))
                 (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c)
               ) :: aux (n+1) impl' subscopes' eargs rargs
 	  end
@@ -1924,8 +1925,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   and smart_gapp f loc = function
     | [] -> f
     | l -> match f with
-      | (loc', GApp (g, args)) -> Loc.tag ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l)
-      | _ -> Loc.tag ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l)
+      | { loc = loc'; v = GApp (g, args) } -> CAst.make ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l)
+      | _ -> CAst.make ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l)
 
   and intern_args env subscopes = function
     | [] -> []
-- 
cgit v1.2.3


From 209956322367e5a4a4c8c78c053ea9352a9a16c8 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Fri, 28 Apr 2017 14:31:14 +0200
Subject: [location] Renaming "CAst.ast" to "CAst.t"

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7dc364e5d9..3b3dccc998 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -893,7 +893,7 @@ type raw_cases_pattern_expr_r =
   (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
   | RCPatAtom  of Id.t option
   | RCPatOr    of raw_cases_pattern_expr list
-and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.ast
+and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.t
 
 (** {6 Elementary bricks } *)
 let apply_scope_env env = function
-- 
cgit v1.2.3