Merge PR #6831: [located] More work towards using CAst.t

7 files changed, 53 insertions, 49 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 10e2592094..a5b7a9e6f0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -347,7 +347,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
 
 let find_tomatch_tycon evdref env loc = function
   (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,(ind,realnal)) ->
+  | Some {CAst.v=(ind,realnal)} ->
       mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal)
   | None ->
       empty_tycon,None
@@ -1565,7 +1565,7 @@ substituer après par les initiaux *)
  * and linearizing the _ patterns.
  * Syntactic correctness has already been done in constrintern *)
 let matx_of_eqns env eqns =
-  let build_eqn (loc,(ids,initial_lpat,initial_rhs)) =
+  let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} =
     let avoid = ids_of_named_context_val (named_context_val env) in
     let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
@@ -1883,8 +1883,8 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
 	    | None -> let sign = match bo with
 		       | None -> [LocalAssum (na, lift n typ)]
 		       | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign
-	    | Some (loc,_) ->
- 	    user_err ?loc 
+            | Some {CAst.loc} ->
+            user_err ?loc
                 (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
@@ -1894,7 +1894,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
 	  let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
 	  let realnal, realnal' =
 	    match t with
-	      | Some (loc,(ind',realnal)) ->
+              | Some {CAst.loc;v=(ind',realnal)} ->
 		  if not (eq_ind ind ind') then
 		    user_err ?loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f98a3b0dbe..8fab92779b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -279,7 +279,7 @@ let _ =
       optwrite = (fun b -> print_allow_match_default_clause := b) }
 
 let rec join_eqns (ids,rhs as x) patll = function
-  | (loc,(ids',patl',rhs') as eqn')::rest ->
+  | ({CAst.loc; v=(ids',patl',rhs')} as eqn')::rest ->
      if not !Flags.raw_print && !print_factorize_match_patterns &&
         List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs'
      then
@@ -290,9 +290,9 @@ let rec join_eqns (ids,rhs as x) patll = function
   | [] ->
      patll, []
 
-let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll
+let number_of_patterns {CAst.v=(_ids,patll,_rhs)} = List.length patll
 
-let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = []
+let is_default_candidate {CAst.v=(ids,_patll,_rhs)} = ids = []
 
 let rec move_more_factorized_default_candidate_to_end eqn n = function
   | eqn' :: eqns ->
@@ -316,22 +316,26 @@ let rec select_default_clause = function
   | [] -> None, []
 
 let factorize_eqns eqns =
+  let open CAst in
   let rec aux found = function
-  | (loc,(ids,patl,rhs))::rest ->
+  | {loc;v=(ids,patl,rhs)}::rest ->
      let patll,rest = join_eqns (ids,rhs) [patl] rest in
-     aux ((loc,(ids,patll,rhs))::found) rest
+     aux (CAst.make ?loc (ids,patll,rhs)::found) rest
   | [] ->
      found in
   let eqns = aux [] (List.rev eqns) in
   let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in
+  let open CAst in
   if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then
     match select_default_clause eqns with
     (* At least two clauses and the last one is disjunctive with no variables *)
-    | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)]
+    | Some {loc=gloc;v=([],patl::_::_,rhs)}, (_::_ as eqns) ->
+      eqns@[CAst.make ?loc:gloc ([],[mk_anon patl],rhs)]
     (* Only one clause which is disjunctive with no variables: we keep at least one constructor *)
     (* so that it is not interpreted as a dummy "match" *)
-    | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)]
-    | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false
+    | Some {loc=gloc;v=([],patl::patl'::_,rhs)}, [] ->
+      [CAst.make ?loc:gloc ([],[patl;mk_anon patl'],rhs)]
+    | Some {v=((_::_,_,_ | _,([]|[_]),_))}, _ -> assert false
     | None, eqns -> eqns
   else
     eqns
@@ -460,7 +464,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
         | _ -> Anonymous, typ in
       let aliastyp =
         if List.for_all (Name.equal Anonymous) nl then None
-        else Some (Loc.tag (indsp,nl)) in
+        else Some (CAst.make (indsp,nl)) in
       n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -726,7 +730,8 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
     let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
-    List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c))
+    List.map (fun (ids,pat,((avoid,env),c)) ->
+        CAst.make (Id.Set.elements ids,[pat],detype d flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
     Array.to_list
@@ -743,7 +748,7 @@ and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs br
   in
   let rec buildrec ids patlist avoid env l b =
     match EConstr.kind sigma b, l with
-      | _, [] -> Loc.tag @@
+      | _, [] -> CAst.make @@
         (Id.Set.elements ids,
          [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)],
          detype d flags avoid env sigma b)
@@ -934,22 +939,23 @@ let rec subst_glob_constr subst = DAst.map (function
 	  GLetIn (n,r1',t',r2')
 
   | GCases (sty,rtno,rl,branches) as raw ->
+    let open CAst in
       let rtno' = Option.smartmap (subst_glob_constr subst) rtno
       and rl' = List.smartmap (fun (a,x as y) ->
         let a' = subst_glob_constr subst a in
         let (n,topt) = x in
         let topt' = Option.smartmap
-          (fun ((loc,((sp,i),y) as t)) ->
+          (fun ({loc;v=((sp,i),y)} as t) ->
             let sp' = subst_mind subst sp in
-            if sp == sp' then t else (loc,((sp',i),y))) topt in
+            if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = List.smartmap
-			(fun (loc,(idl,cpl,r) as branch) ->
+                        (fun ({loc;v=(idl,cpl,r)} as branch) ->
 			   let cpl' =
 			     List.smartmap (subst_cases_pattern subst) cpl
 			   and r' = subst_glob_constr subst r in
 			     if cpl' == cpl && r' == r then branch else
-			       (loc,(idl,cpl',r')))
+                               CAst.(make ?loc (idl,cpl',r')))
 			branches
       in
 	if rtno' == rtno && rl' == rl && branches' == branches then raw else
@@ -1014,9 +1020,9 @@ let simple_cases_matrix_of_branches ind brs =
       let mkPatVar na = DAst.make @@ PatVar na in
       let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
       let ids = List.map_filter Nameops.Name.to_option nal in
-      Loc.tag @@ (ids,[p],c))
+      CAst.make @@ (ids,[p],c))
     brs
 
 let return_type_of_predicate ind nrealargs_tags pred =
   let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in
-  (List.hd nal, Some (Loc.tag (ind, List.tl nal))), Some p
+  (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 2280ee2d47..74f2cefab6 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Util
+open CAst
 open Names
 open Nameops
 open Globnames
@@ -34,7 +35,7 @@ let set_pat_alias id = DAst.map (function
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
-    | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml)
+    | (tm,(na,Some {v=(_,nal)})) -> na::nal) tml)
 
 let mkGApp ?loc p t = DAst.make ?loc @@
   match DAst.get p with
@@ -79,13 +80,13 @@ let matching_var_kind_eq k1 k2 = match k1, k2 with
 | (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false
 
 let tomatch_tuple_eq f (c1, p1) (c2, p2) =
-  let eqp (_, (i1, na1)) (_, (i2, na2)) =
+  let eqp {CAst.v=(i1, na1)} {CAst.v=(i2, na2)} =
     eq_ind i1 i2 && List.equal Name.equal na1 na2
   in
   let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
   f c1 c2 && eq_pred p1 p2
 
-and cases_clause_eq f (_, (id1, p1, c1)) (_, (id2, p2, c2)) =
+and cases_clause_eq f {CAst.v=(id1, p1, c1)} {CAst.v=(id2, p2, c2)} =
   List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2
 
 let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
@@ -173,7 +174,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
   | GCases (sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in
       let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
-      let comp3 = Util.List.map_left (fun (loc,(idl,p,c)) -> (loc,(idl,p,f c))) pl in
+      let comp3 = Util.List.map_left (CAst.map (fun (idl,p,c) -> (idl,p,f c))) pl in
       GCases (sty,comp1,comp2,comp3)
   | GLetTuple (nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
@@ -211,7 +212,7 @@ let fold_glob_constr f acc = DAst.with_val (function
   | GLetIn (_,b,t,c) ->
     f (Option.fold_left f (f acc b) t) c
   | GCases (_,rtntypopt,tml,pl) ->
-    let fold_pattern acc (_,(idl,p,c)) = f acc c in
+    let fold_pattern acc {CAst.v=(idl,p,c)} = f acc c in
     List.fold_left fold_pattern
       (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml))
       pl
@@ -244,9 +245,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GLetIn (na,b,t,c) ->
     f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c
   | GCases (_,rtntypopt,tml,pl) ->
-    let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in
+    let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in
     let fold_tomatch (v',acc) (tm,(na,onal)) =
-      (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'')
+      (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
                         (Name.fold_right g na v') onal,
        f v acc tm) in
     let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
@@ -336,10 +337,10 @@ let bound_glob_vars =
    probably be no significant penalty in doing reallocation as
    pattern-matching expressions are usually rather small. *)
 
-let map_inpattern_binders f ((loc,(id,nal)) as x) =
+let map_inpattern_binders f ({loc;v=(id,nal)} as x) =
   let r = CList.smartmap f nal in
   if r == nal then x
-  else loc,(id,r)
+  else CAst.make ?loc (id,r)
 
 let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple =
   let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in
@@ -360,14 +361,14 @@ let rec map_case_pattern_binders f = DAst.map (function
       else PatCstr(c,rps,rna)
   )
 
-let map_cases_branch_binders f ((loc,(il,cll,rhs)) as x) : cases_clause =
+let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause =
   (* spiwack: not sure if I must do something with the list of idents.
      It is intended to be a superset of the free variable of the
      right-hand side, if I understand correctly. But I'm not sure when
      or how they are used. *)
   let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in
   if r == cll then x
-  else loc,(il,r,rhs)
+  else CAst.make ?loc (il,r,rhs)
 
 let map_pattern_binders f tomatch branches =
   CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch,
@@ -377,8 +378,8 @@ let map_pattern_binders f tomatch branches =
 
 let map_tomatch f (c,pp) : tomatch_tuple = f c , pp
 
-let map_cases_branch f (loc,(il,cll,rhs)) : cases_clause =
-  loc , (il , cll , f rhs)
+let map_cases_branch f =
+  CAst.map (fun (il,cll,rhs) -> (il , cll , f rhs))
 
 let map_pattern f tomatch branches =
   List.map (fun tm -> map_tomatch f tm) tomatch,
@@ -437,11 +438,11 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
   (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
   | GCases (ci,po,tomatchl,cls) ->
       let test_pred_pat (na,ino) =
-        test_na l na; Option.iter (fun (_,(_,nal)) -> List.iter (test_na l) nal) ino in
+        test_na l na; Option.iter (fun {v=(_,nal)} -> List.iter (test_na l) nal) ino in
       let test_clause idl = List.iter (test_id l) idl in
       let po = Option.map (rename_glob_vars l) po in
       let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
-      let cls = Util.List.map_left (fun (loc,(idl,p,c)) -> test_clause idl; (loc,(idl,p,rename_glob_vars l c))) cls in
+      let cls = Util.List.map_left (CAst.map (fun (idl,p,c) -> test_clause idl; (idl,p,rename_glob_vars l c))) cls in
       GCases (ci,po,tomatchl,cls)
   | GLetTuple (nal,(na,po),c,b) ->
      List.iter (test_na l) (na::nal);
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index c5ce0496bc..0f0af5409e 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -65,7 +65,7 @@ let map_red_expr_gen f g h = function
 (** Mapping bindings *)
 
 let map_explicit_bindings f l =
-  let map (loc, (hyp, x)) = (loc, (hyp, f x)) in
+  let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in
   List.map map l
 
 let map_bindings f = function
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3fab553cb0..dcb93bfb62 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -416,17 +416,17 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       | _ -> None
       in
       let get_ind = function
-	| (_,(_,[p],_))::_ -> get_ind p
+        | {CAst.v=(_,[p],_)}::_ -> get_ind p
 	| _ -> None
       in
       let ind_tags,ind = match indnames with
-	| Some (_,(ind,nal)) -> Some (List.length nal), Some ind
+        | Some {CAst.v=(ind,nal)} -> Some (List.length nal), Some ind
 	| None -> None, get_ind brs
       in
       let ext,brs = pats_of_glob_branches loc metas vars ind brs
       in
       let pred = match p,indnames with
-	| Some p, Some (_,(_,nal)) ->
+        | Some p, Some {CAst.v=(_,nal)} ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
         | None, _ -> PMeta None
@@ -462,7 +462,7 @@ and pats_of_glob_branches loc metas vars ind brs =
   in
   let rec get_pat indexes = function
     | [] -> false, []
-    | (loc',(_,[p], br)) :: brs ->
+    | {CAst.loc=loc';v=(_,[p], br)} :: brs ->
       begin match DAst.get p, DAst.get br, brs with
       | PatVar Anonymous, GHole _, [] ->
         true, [] (* ends with _ => _ *)
@@ -484,7 +484,7 @@ and pats_of_glob_branches loc metas vars ind brs =
       | _ ->
         err ?loc:loc' (Pp.str "Non supported pattern.")
       end
-    | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.")
+    | {CAst.loc;v=(_,_,_)} :: _ -> err ?loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 6475388f9e..e10c81c24a 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 (*i*)
-open Names
 open EConstr
 open Environ
 open Constrexpr
@@ -20,7 +19,7 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
-    | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
+    | UnboundMethod of global_reference * Misctypes.lident (* Class name, method *)
     | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index ce647029f9..d98295658f 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Loc
-open Names
 open EConstr
 open Environ
 open Constrexpr
@@ -19,14 +17,14 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
-  | UnboundMethod of global_reference * Id.t located (** Class name, method *)
+  | UnboundMethod of global_reference * Misctypes.lident (** Class name, method *)
   | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
 val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> global_reference -> Id.t located -> 'a
+val unbound_method : env -> global_reference -> Misctypes.lident -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a