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

1 files changed, 60 insertions, 57 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 966ba6734..a99c0951f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -213,11 +213,11 @@ let tag_var = tag Tag.variable
         str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
   let pr_opt_type pr = function
-    | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
+    | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> mt ()
     | t -> cut () ++ str ":" ++ pr t
 
   let pr_opt_type_spc pr = function
-    | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
+    | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
   let pr_lident (loc,id) =
@@ -352,7 +352,7 @@ let tag_var = tag Tag.variable
         end
       | Default b ->
         match t with
-          | CHole (_,_,Misctypes.IntroAnonymous,_) ->
+          | _loc, CHole (_,Misctypes.IntroAnonymous,_) ->
             let s = prlist_with_sep spc pr_lname nal in
             hov 1 (surround_implicit b s)
           | _ ->
@@ -394,39 +394,40 @@ let tag_var = tag Tag.variable
   (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
       if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
-    | CProdN (loc,[],c) ->
+    | _loc, CProdN ([],c) ->
       extract_prod_binders c
-    | CProdN (loc,[[_,Name id],bk,t],
-              CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))]))
+    | loc, CProdN ([[_,Name id],bk,t],
+              (_loc', CCases (LetPatternStyle,None, [(_loc'', CRef (Ident (_,id'),None)),None,None],[(_,([_,[p]],b))])))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
-      CLocalPattern (loc,p,None) :: bl, c
-    | CProdN (loc,(nal,bk,t)::bl,c) ->
-      let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
+      CLocalPattern (loc, p,None) :: bl, c
+    | loc, CProdN ((nal,bk,t)::bl,c) ->
+      let bl,c = extract_prod_binders (loc, CProdN(bl,c)) in
       CLocalAssum (nal,bk,t) :: bl, c
     | c -> [], c
 
-  let rec extract_lam_binders = function
+  let rec extract_lam_binders (loc, ce) = match ce with
   (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_lam_binders c in
       if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
-    | CLambdaN (loc,[],c) ->
+    | CLambdaN ([],c) ->
       extract_lam_binders c
-    | CLambdaN (loc,[[_,Name id],bk,t],
-                CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))]))
+    | CLambdaN ([[_,Name id],bk,t],
+                (_loc, CCases (LetPatternStyle,None, [(_loc', CRef (Ident (_,id'),None)),None,None],[(_,([_,[p]],b))])))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
       CLocalPattern (loc,p,None) :: bl, c
-    | CLambdaN (loc,(nal,bk,t)::bl,c) ->
-      let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
+    | CLambdaN ((nal,bk,t)::bl,c) ->
+      let bl,c = extract_lam_binders (loc, CLambdaN(bl,c)) in
       CLocalAssum (nal,bk,t) :: bl, c
-    | c -> [], c
+    | c -> [], Loc.tag ~loc c
 
-  let split_lambda = function
-    | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
-    | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
-    | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
+  let split_lambda = Loc.with_loc (fun ~loc -> function
+    | CLambdaN ([[na],bk,t],c) -> (na,t,c)
+    | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN(bl,c))
+    | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN((nal,bk,t)::bl,c))
     | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+    )
 
   let rename na na' t c =
     match (na,na') with
@@ -435,12 +436,13 @@ let tag_var = tag Tag.variable
       | (_,Name id), (_,Anonymous) -> (na,t,c)
       | _ -> (na',t,c)
 
-  let split_product na' = function
-    | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
-    | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
-    | CProdN (loc,(na::nal,bk,t)::bl,c) ->
-      rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
+  let split_product na' = Loc.with_loc (fun ~loc -> function
+    | CProdN ([[na],bk,t],c) -> rename na na' t c
+    | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ~loc @@ CProdN(bl,c))
+    | CProdN ((na::nal,bk,t)::bl,c) ->
+      rename na na' t (Loc.tag ~loc @@ CProdN((nal,bk,t)::bl,c))
     | _ -> anomaly (Pp.str "ill-formed fixpoint body")
+    )
 
   let rec split_fix n typ def =
     if Int.equal n 0 then ([],typ,def)
@@ -506,7 +508,7 @@ let tag_var = tag Tag.variable
 
   let pr_case_type pr po =
     match po with
-      | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt()
+      | None | Some (_, CHole (_,Misctypes.IntroAnonymous,_)) -> mt()
       | Some p ->
         spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p)
 
@@ -543,25 +545,25 @@ let tag_var = tag Tag.variable
   let pr_fun_sep = spc () ++ str "=>"
 
   let pr_dangling_with_for sep pr inherited a =
-    match a with
-      | (CFix (_,_,[_])|CCoFix(_,_,[_])) ->
+    match snd a with
+      | (CFix (_,[_])|CCoFix(_,[_])) ->
         pr sep (latom,E) a
       | _ ->
         pr sep inherited a
 
   let pr pr sep inherited a =
     let return (cmds, prec) = (tag_constr_expr a cmds, prec) in
-    let (strm, prec) = match a with
+    let (strm, prec) = match snd @@ Loc.to_pair a with
       | CRef (r, us) ->
         return (pr_cref r us, latom)
-      | CFix (_,id,fix) ->
+      | CFix (id,fix) ->
         return (
           hov 0 (keyword "fix" ++ spc () ++
                    pr_recursive
                    (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
           lfix
         )
-      | CCoFix (_,id,cofix) ->
+      | CCoFix (id,cofix) ->
         return (
           hov 0 (keyword "cofix" ++ spc () ++
                    pr_recursive
@@ -586,7 +588,8 @@ let tag_var = tag Tag.variable
               pr_fun_sep ++ pr spc ltop a),
           llambda
         )
-      | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b)
+      | CLetIn ((_,Name x), ((_loc, CFix((_,x'),[_]))
+                          |  (_loc, CCoFix((_,x'),[_])) as fx), t, b)
           when Id.equal x x' ->
         return (
           hv 0 (
@@ -596,7 +599,7 @@ let tag_var = tag Tag.variable
               pr spc ltop b),
           lletin
         )
-      | CLetIn (_,x,a,t,b) ->
+      | CLetIn (x,a,t,b) ->
         return (
           hv 0 (
             hov 2 (keyword "let" ++ spc () ++ pr_lname x
@@ -606,7 +609,7 @@ let tag_var = tag Tag.variable
               pr spc ltop b),
           lletin
         )
-      | CAppExpl (_,(Some i,f,us),l) ->
+      | CAppExpl ((Some i,f,us),l) ->
         let l1,l2 = List.chop i l in
         let c,l1 = List.sep_last l1 in
         let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
@@ -614,16 +617,16 @@ let tag_var = tag Tag.variable
           return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
         else
           return (p, lproj)
-      | CAppExpl (_,(None,Ident (_,var),us),[t])
-      | CApp (_,(_,CRef(Ident(_,var),us)),[t,None])
+      | CAppExpl ((None,Ident (_,var),us),[t])
+      | CApp ((_,(_, CRef(Ident(_,var),us))),[t,None])
           when Id.equal var Notation_ops.ldots_var ->
         return (
           hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
           larg
         )
-      | CAppExpl (_,(None,f,us),l) ->
+      | CAppExpl ((None,f,us),l) ->
         return (pr_appexpl (pr mt) (f,us) l, lapp)
-      | CApp (_,(Some i,f),l) ->
+      | CApp ((Some i,f),l) ->
         let l1,l2 = List.chop i l in
         let c,l1 = List.sep_last l1 in
         assert (Option.is_empty (snd c));
@@ -635,14 +638,14 @@ let tag_var = tag Tag.variable
           )
         else
           return (p, lproj)
-      | CApp (_,(None,a),l) ->
+      | CApp ((None,a),l) ->
         return (pr_app (pr mt) a l, lapp)
-      | CRecord (_,l) ->
+      | CRecord l ->
         return (
           hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
           latom
         )
-      | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
+      | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
@@ -653,7 +656,7 @@ let tag_var = tag Tag.variable
                        spc () ++ keyword "in" ++ pr spc ltop b)),
           lletpattern
         )
-      | CCases(_,_,rtntypopt,c,eqns) ->
+      | CCases(_,rtntypopt,c,eqns) ->
         return (
           v 0
             (hv 0 (keyword "match" ++ brk (1,2) ++
@@ -666,7 +669,7 @@ let tag_var = tag Tag.variable
              ++ keyword "end"),
           latom
         )
-      | CLetTuple (_,nal,(na,po),c,b) ->
+      | CLetTuple (nal,(na,po),c,b) ->
         return (
           hv 0 (
             hov 2 (keyword "let" ++ spc () ++
@@ -679,7 +682,7 @@ let tag_var = tag Tag.variable
               pr spc ltop b),
           lletin
         )
-      | CIf (_,c,(na,po),b1,b2) ->
+      | CIf (c,(na,po),b1,b2) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
          parsing est lui plus tolérant) *)
         return (
@@ -693,19 +696,19 @@ let tag_var = tag Tag.variable
         lif
         )
 
-      | CHole (_,_,Misctypes.IntroIdentifier id,_) ->
+      | CHole (_,Misctypes.IntroIdentifier id,_) ->
         return (str "?[" ++ pr_id id ++ str "]", latom)
-      | CHole (_,_,Misctypes.IntroFresh id,_) ->
+      | CHole (_,Misctypes.IntroFresh id,_) ->
         return (str "?[?" ++ pr_id id ++ str "]", latom)
-      | CHole (_,_,_,_) ->
+      | CHole (_,_,_) ->
         return (str "_", latom)
-      | CEvar (_,n,l) ->
+      | CEvar (n,l) ->
         return (pr_evar (pr mt) n l, latom)
-      | CPatVar (_,p) ->
+      | CPatVar p ->
         return (str "@?" ++ pr_patvar p, latom)
-      | CSort (_,s) ->
+      | CSort s ->
         return (pr_glob_sort s, latom)
-      | CCast (_,a,b) ->
+      | CCast (a,b) ->
         return (
           hv 0 (pr mt (lcast,L) a ++ spc () ++
                   match b with
@@ -715,15 +718,15 @@ let tag_var = tag Tag.variable
                     | CastCoerce -> str ":>"),
           lcast
         )
-      | CNotation (_,"( _ )",([t],[],[])) ->
+      | CNotation ("( _ )",([t],[],[])) ->
         return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
-      | CNotation (_,s,env) ->
+      | CNotation (s,env) ->
         pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env
-      | CGeneralization (_,bk,ak,c) ->
+      | CGeneralization (bk,ak,c) ->
         return (pr_generalization bk ak (pr mt ltop c), latom)
-      | CPrim (_,p) ->
+      | CPrim p ->
         return (pr_prim_token p, prec_of_prim_token p)
-      | CDelimiters (_,sc,a) ->
+      | CDelimiters (sc,a) ->
         return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
     in
     let loc = constr_loc a in
@@ -751,7 +754,7 @@ let tag_var = tag Tag.variable
   let pr prec c = pr prec (transf (Global.env()) c)
 
   let pr_simpleconstr = function
-    | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us
+    | _lock, CAppExpl ((None,f,us),[]) -> str "@" ++ pr_cref f us
     | c -> pr lsimpleconstr c
 
   let default_term_pr = {