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

11 files changed, 494 insertions, 113 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
new file mode 100644
index 000000000..2415080f3
--- /dev/null
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -0,0 +1,387 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+DECLARE PLUGIN "decl_mode_plugin"
+
+open Ltac_plugin
+open Compat
+open Pp
+open Decl_expr
+open Names
+open Pcoq
+open Vernacexpr
+open Tok (* necessary for camlp4 *)
+
+open Pcoq.Constr
+open Pltac
+open Ppdecl_proof
+
+let pr_goal gs =
+  let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
+  let env = Goal.V82.env sigma g in
+  let concl = Goal.V82.concl sigma g in
+  let goal =
+    Printer.pr_context_of env sigma ++ cut () ++
+      str "============================" ++ cut ()  ++
+      str "thesis :=" ++ cut () ++
+      Printer.pr_goal_concl_style_env env sigma concl in
+  str "     *** Declarative Mode ***" ++ fnl () ++ fnl () ++
+    str "  " ++ v 0 goal
+
+let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
+  match gll with
+  | [goal] when pr_first ->
+      pr_goal { Evd.it = goal ; sigma = sigma }
+  | _ ->
+      (* spiwack: it's not very nice to have to call proof global
+         here, a more robust solution would be to add a hook for
+         [Printer.pr_open_subgoals] in proof modes, in order to
+         compute the end command. Yet a more robust solution would be
+         to have focuses give explanations of their unfocusing
+         behaviour. *)
+      let p = Proof_global.give_me_the_proof () in
+      let close_cmd = Decl_mode.get_end_command p in
+      str "Subproof completed, now type " ++ str close_cmd ++ str "."
+
+let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
+  Decl_interp.interp_proof_instr 
+    (Decl_mode.get_info sigma gl)
+    (Goal.V82.env sigma gl)
+    (sigma)
+
+let vernac_decl_proof () = 
+  let pf = Proof_global.give_me_the_proof () in
+  if Proof.is_done pf then 
+    CErrors.error "Nothing left to prove here."
+  else
+    begin
+      Decl_proof_instr.go_to_proof_mode () ;
+      Proof_global.set_proof_mode "Declarative"
+    end
+
+(* spiwack: some bureaucracy is not performed here *)
+let vernac_return () =
+  begin
+    Decl_proof_instr.return_from_tactic_mode () ;
+    Proof_global.set_proof_mode "Declarative"
+  end
+
+let vernac_proof_instr instr =
+  Decl_proof_instr.proof_instr instr
+
+(* Before we can write an new toplevel command (see below) 
+    which takes a [proof_instr] as argument, we need to declare
+    how to parse it, print it, globalise it and interprete it.
+    Normally we could do that easily through ARGUMENT EXTEND, 
+    but as the parsing is fairly complicated we will do it manually to
+    indirect through the [proof_instr] grammar entry. *)
+(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
+
+(* Only declared at raw level, because only used in vernac commands. *)
+let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
+  Genarg.make0 "proof_instr"
+
+(* We create a new parser entry [proof_mode]. The Declarative proof mode
+    will replace the normal parser entry for tactics with this one. *)
+let proof_mode : vernac_expr Gram.entry =
+  Gram.entry_create "vernac:proof_command"
+(* Auxiliary grammar entry. *)
+let proof_instr : raw_proof_instr Gram.entry =
+  Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
+
+let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
+  pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
+
+let classify_proof_instr = function
+  | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
+  | _ -> Vernac_classifier.classify_as_proofstep
+
+(* We use the VERNAC EXTEND facility with a custom non-terminal
+    to populate [proof_mode] with a new toplevel interpreter.
+    The "-" indicates that the rule does not start with a distinguished
+    string. *)
+VERNAC proof_mode EXTEND ProofInstr
+  [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ]
+END
+
+(* It is useful to use GEXTEND directly to call grammar entries that have been
+    defined previously VERNAC EXTEND. In this case we allow, in proof mode,
+    the use of commands like Check or Print. VERNAC EXTEND does quite a bit of
+    bureaucracy for us, but it is not needed in this sort of case, and it would require
+    to have an ARGUMENT EXTEND version of the "proof_mode" grammar entry. *)
+GEXTEND Gram
+  GLOBAL: proof_mode ;
+
+  proof_mode: LAST
+    [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ]
+  ;
+END  
+
+(* We register a new proof mode here *)
+
+let _ = 
+  Proof_global.register_proof_mode { Proof_global.
+				       name = "Declarative" ; (* name for identifying and printing *)
+				       (* function [set] goes from No Proof Mode to 
+					   Declarative Proof Mode performing side effects *)
+				       set = begin fun () ->
+					 (* We set the command non terminal to
+					     [proof_mode] (which we just defined). *)
+					 Pcoq.set_command_entry proof_mode ;
+					 (* We substitute the goal printer, by the one we built
+					     for the proof mode. *)
+					 Printer.set_printer_pr { Printer.default_printer_pr with
+								                Printer.pr_goal = pr_goal;
+                                                                                pr_subgoals = pr_subgoals; }
+				       end ;
+                                       (* function [reset] goes back to No Proof Mode from
+					   Declarative Proof Mode *)
+				       reset = begin fun () ->
+					 (* We restore the command non terminal to
+					      [noedit_mode]. *)
+					 Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
+					 (* We restore the goal printer to default *)
+					 Printer.set_printer_pr Printer.default_printer_pr
+				       end
+				   }
+
+VERNAC COMMAND EXTEND DeclProof
+[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
+END
+VERNAC COMMAND EXTEND  DeclReturn
+[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ]
+END
+
+let none_is_empty = function
+    None -> []
+  | Some l -> l
+
+GEXTEND Gram
+GLOBAL: proof_instr;
+  thesis :
+    [[ "thesis" -> Plain 
+     | "thesis"; "for"; i=ident -> (For i)
+     ]];
+  statement :
+    [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
+     | i=ident -> {st_label=Anonymous;
+		   st_it= Loc.tag ~loc:!@loc @@ Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
+     | c=constr -> {st_label=Anonymous;st_it=c}
+     ]];
+  constr_or_thesis :
+     [[ t=thesis -> Thesis t ] |
+      [ c=constr -> This c
+      ]];
+  statement_or_thesis : 
+    [
+      [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] 
+    |
+      [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
+      | i=ident -> {st_label=Anonymous;
+		    st_it=This (Loc.tag ~loc:!@loc @@ Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
+      | c=constr -> {st_label=Anonymous;st_it=This c}
+      ]
+    ];
+  justification_items : 
+    [[ -> Some [] 
+     | "by"; l=LIST1 constr SEP "," -> Some l
+     | "by"; "*"                    -> None ]]
+  ;
+  justification_method : 
+    [[ -> None 
+     | "using";  tac = tactic -> Some tac ]]
+  ;
+  simple_cut_or_thesis :
+    [[ ls = statement_or_thesis;
+       j = justification_items;
+       taco = justification_method 	
+	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
+  ;
+  simple_cut :
+    [[ ls = statement;
+       j = justification_items;
+       taco = justification_method 	
+	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
+  ;
+  elim_type:
+    [[ IDENT "induction" -> ET_Induction
+     | IDENT "cases" -> ET_Case_analysis ]]
+  ;
+  block_type :
+    [[ IDENT "claim" -> B_claim
+     | IDENT "focus" -> B_focus
+     | IDENT "proof" -> B_proof
+     | et=elim_type -> B_elim et ]]
+  ;    
+  elim_obj:
+    [[ IDENT "on"; c=constr -> Real c
+     | IDENT "of"; c=simple_cut -> Virtual c ]]
+  ;  
+  elim_step:
+    [[ IDENT "consider" ; 
+       h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h)
+     | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)
+     | IDENT "suffices"; ls=suff_clause;
+       j = justification_items;
+       taco = justification_method 	
+	-> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] 
+  ;
+  rew_step :
+    [[ "~=" ;         c=simple_cut -> (Rhs,c)       
+     | "=~" ;         c=simple_cut -> (Lhs,c)]]
+  ;
+  cut_step:
+    [[ "then"; tt=elim_step -> Pthen tt
+     | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c)
+     | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) 
+     | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c)
+     | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c)
+     | tt=elim_step -> tt
+     | tt=rew_step -> let s,c=tt in Prew (s,c); 
+     | IDENT "have"; c=simple_cut_or_thesis -> Pcut c;
+     | IDENT "claim"; c=statement -> Pclaim c;
+     | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c;    
+     | "end"; bt = block_type -> Pend bt;
+     | IDENT "escape" -> Pescape ]]
+  ;
+  (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*)
+  loc_id: 
+    [[ id=ident -> fun x -> (!@loc,(id,x)) ]];
+  hyp:
+    [[ id=loc_id -> id None ;
+     | id=loc_id ; ":" ; c=constr -> id (Some c)]]
+  ;
+  consider_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=consider_vars -> (Hvar name) :: v
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h
+     ]]
+  ;
+  consider_hyps:  
+    [[ st=statement; IDENT "and"; h=consider_hyps  -> Hprop st::h
+     | st=statement; IDENT "and"; 
+       IDENT "consider" ; v=consider_vars  -> Hprop st::v
+     | st=statement -> [Hprop st]
+     ]]
+  ;  
+  assume_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=assume_vars -> (Hvar name) :: v
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h
+     ]]
+  ;
+  assume_hyps:  
+    [[ st=statement; IDENT "and"; h=assume_hyps  -> Hprop st::h
+     | st=statement; IDENT "and"; 
+       IDENT "we"; IDENT "have" ; v=assume_vars  -> Hprop st::v
+     | st=statement -> [Hprop st]
+     ]]
+  ;
+  assume_clause:
+    [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v
+    |  h=assume_hyps -> h ]]
+  ; 
+  suff_vars:
+    [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis ->
+      [Hvar name],c
+     | name=hyp; ","; v=suff_vars -> 
+	 let (q,c) = v in ((Hvar name) :: q),c
+     | name=hyp; 
+       IDENT "such"; IDENT "that"; h=suff_hyps -> 
+	 let (q,c) = h in ((Hvar name) :: q),c
+     ]];
+  suff_hyps:  
+    [[ st=statement; IDENT "and"; h=suff_hyps  ->	 
+	 let (q,c) = h in (Hprop st::q),c
+     | st=statement; IDENT "and"; 
+       IDENT "to" ; IDENT "have" ; v=suff_vars -> 
+	 let (q,c) = v in (Hprop st::q),c
+     | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> 
+	 [Hprop st],c
+     ]]
+  ;
+  suff_clause:
+    [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v
+    |  h=suff_hyps -> h ]]
+  ; 
+  let_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=let_vars -> (Hvar name) :: v
+     | name=hyp; IDENT "be"; 
+       IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h
+     ]]
+  ;
+  let_hyps:  
+    [[ st=statement; IDENT "and"; h=let_hyps  -> Hprop st::h
+    |  st=statement; IDENT "and"; "let"; v=let_vars  -> Hprop st::v
+    |  st=statement -> [Hprop st]
+    ]];
+  given_vars:
+    [[ name=hyp -> [Hvar name]
+     | name=hyp; ","; v=given_vars -> (Hvar name) :: v
+     | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h
+     ]]
+  ;
+  given_hyps:  
+    [[ st=statement; IDENT "and"; h=given_hyps  -> Hprop st::h
+    |  st=statement; IDENT "and"; IDENT "given"; v=given_vars  -> Hprop st::v
+    |  st=statement -> [Hprop st]
+    ]];
+  suppose_vars:
+    [[name=hyp -> [Hvar name] 
+     |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v
+     |name=hyp; OPT[IDENT "be"]; 
+      IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h
+     ]]
+  ;
+  suppose_hyps:  
+    [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h
+     | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have";
+          v=suppose_vars -> Hprop st::v
+     | st=statement_or_thesis -> [Hprop st]
+     ]]
+  ;
+  suppose_clause:
+    [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v;
+     |  h=suppose_hyps -> h ]]
+  ;
+  intro_step:
+    [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
+     | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
+       po=OPT[ "with"; p=LIST1 hyp SEP ","-> p  ] ; 
+       ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> 
+	 Pcase (none_is_empty po,c,none_is_empty ho)
+     | "let" ; v=let_vars -> Plet v	 
+     | IDENT "take"; witnesses = LIST1 constr SEP ","  -> Ptake witnesses
+     | IDENT "assume"; h=assume_clause -> Passume h
+     | IDENT "given"; h=given_vars -> Pgiven h
+     | IDENT "define"; id=ident; args=LIST0 hyp; 
+       "as"; body=constr -> Pdefine(id,args,body)
+     | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ)
+     | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ)
+     ]]
+  ;
+  emphasis : 
+    [[ -> 0
+     | "*" -> 1
+     | "**" -> 2
+     | "***" -> 3
+     ]]
+  ;
+  bare_proof_instr:
+    [[ c = cut_step -> c ;
+     | i = intro_step -> i ]]
+  ;
+  proof_instr :
+    [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]]
+  ;
+END;;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7dc869131..4b942c989 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1247,16 +1247,15 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_
   in
   List.rev !l
 
-let rec rebuild_return_type rt =
+let rec rebuild_return_type (loc, rt) =
   match rt with
-    | Constrexpr.CProdN(loc,n,t') ->
-	Constrexpr.CProdN(loc,n,rebuild_return_type t')
-    | Constrexpr.CLetIn(loc,na,v,t,t') ->
-	Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t')
-    | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
-				       Constrexpr.Default Decl_kinds.Explicit,rt],
-			    Constrexpr.CSort(Loc.ghost,GType []))
-
+    | Constrexpr.CProdN(n,t') ->
+        Loc.tag ~loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
+    | Constrexpr.CLetIn(na,v,t,t') ->
+	Loc.tag ~loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
+    | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.ghost,Anonymous],
+				       Constrexpr.Default Decl_kinds.Explicit,Loc.tag ~loc rt],
+			    Loc.tag @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
       evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
@@ -1307,13 +1306,12 @@ let do_build_inductive
 	(fun (n,t,typ) acc ->
           match typ with
           | Some typ ->
-	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	     Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
 	  | None ->
-	     Constrexpr.CProdN
-	       (Loc.ghost,
-		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+	     Loc.tag @@ Constrexpr.CProdN
+	       ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 		acc
 	       )
 	)
@@ -1375,13 +1373,12 @@ let do_build_inductive
       (fun (n,t,typ) acc ->
          match typ with
          | Some typ ->
-	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	   Loc.tag @@ Constrexpr.CLetIn((Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
 	 | None ->
-	   Constrexpr.CProdN
-	   (Loc.ghost,
-	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+           Loc.tag @@ Constrexpr.CProdN
+	   ([[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 	    acc
 	   )
       )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index daa5cbb3f..6ee755323 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -469,8 +469,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   in
   let unbounded_eq =
     let f_app_args =
-      Constrexpr.CAppExpl
-	(Loc.ghost,
+      Loc.tag @@ Constrexpr.CAppExpl(
 	 (None,(Ident (Loc.ghost,fname)),None) ,
 	 (List.map
 	    (function
@@ -481,7 +480,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
+    Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in
@@ -589,15 +588,15 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
 	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') ->
+	  | (Constrexpr.CLocalDef(na,_,_))::bl',(_loc, Constrexpr.CLetIn(_,nat,ty,typ')) ->
 	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
-	match nal,typ with 
+	match nal, snd typ with 
 	  | [], _ -> rebuild_bl (aux,assoc) bl' typ
-	  | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
-	  | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> 
+	  | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
+	  | _,CProdN((nal',bk',nal't)::rest,typ') -> 
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
@@ -607,15 +606,15 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if List.is_empty new_nal' && List.is_empty rest
 		 then typ'
-		 else if List.is_empty new_nal'
-		 then CProdN(Loc.ghost,rest,typ')
-		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
+		 else Loc.tag @@ if List.is_empty new_nal'
+		 then CProdN(rest,typ')
+		 else CProdN(((new_nal',bk',nal't)::rest),typ'))
 	    else 
 	      let captured_nal,non_captured_nal = List.chop lnal' nal in
 	      let nassoc = make_assoc assoc nal' captured_nal in
 	      let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_nal ((assum :: aux), nassoc)
-		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
+		bk bl' non_captured_nal (lnal - lnal') (Loc.tag @@ CProdN(rest,typ'))
 	  | _ -> assert false
 
 let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
@@ -726,67 +725,65 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   in
   ()
 
-let rec add_args id new_args b =
-  match b with
-  | CRef (r,_) ->
-      begin      match r with
+let rec add_args id new_args = Loc.map (function
+  | CRef (r,_) as b ->
+      begin match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
-	    CAppExpl(Loc.ghost,(None,r,None),new_args)
+	    CAppExpl((None,r,None),new_args)
 	| _ -> b
       end
   | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
-  | CProdN(loc,nal,b1) ->
-      CProdN(loc,
-	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+  | CProdN(nal,b1) ->
+        CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
 	     add_args id new_args  b1)
-  | CLambdaN(loc,nal,b1) ->
-      CLambdaN(loc,
-	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
+  | CLambdaN(nal,b1) ->
+      CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
 	       add_args id new_args  b1)
-  | CLetIn(loc,na,b1,t,b2) ->
-      CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
-  | CAppExpl(loc,(pf,r,us),exprl) ->
+  | CLetIn(na,b1,t,b2) ->
+      CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
+  | CAppExpl((pf,r,us),exprl) ->
       begin
 	match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
-	    CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl))
-	| _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl)
+	    CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
+	| _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
       end
-  | CApp(loc,(pf,b),bl) ->
-      CApp(loc,(pf,add_args id new_args b),
+  | CApp((pf,b),bl) ->
+      CApp((pf,add_args id new_args b),
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
-  | CCases(loc,sty,b_option,cel,cal) ->
-      CCases(loc,sty,Option.map (add_args id new_args) b_option,
+  | CCases(sty,b_option,cel,cal) ->
+      CCases(sty,Option.map (add_args id new_args) b_option,
 	     List.map (fun (b,na,b_option) ->
 			 add_args id new_args b,
 			 na, b_option) cel,
-	     List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc:loc @@ (cpl,add_args id new_args e)) cal
+	     List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc @@ (cpl,add_args id new_args e)) cal
 	    )
-  | CLetTuple(loc,nal,(na,b_option),b1,b2) ->
-      CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
+  | CLetTuple(nal,(na,b_option),b1,b2) ->
+      CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
 		add_args id new_args b1,
 		add_args id new_args b2
 	       )
 
-  | CIf(loc,b1,(na,b_option),b2,b3) ->
-      CIf(loc,add_args id new_args b1,
+  | CIf(b1,(na,b_option),b2,b3) ->
+      CIf(add_args id new_args b1,
 	  (na,Option.map (add_args id new_args) b_option),
 	  add_args id new_args b2,
 	  add_args id new_args b3
 	 )
-  | CHole _ -> b
-  | CPatVar _ -> b
-  | CEvar _ -> b
-  | CSort _ -> b
-  | CCast(loc,b1,b2)  ->
-      CCast(loc,add_args id new_args b1,
+  | CHole _
+  | CPatVar _
+  | CEvar _
+  | CPrim _
+  | CSort _ as b -> b
+  | CCast(b1,b2)  ->
+      CCast(add_args id new_args b1,
 	    Miscops.map_cast_type (add_args id new_args) b2)
-  | CRecord (loc, pars) ->
-      CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars)
+  | CRecord pars ->
+      CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
   | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
-  | CPrim _ -> b
   | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
+  )
 exception Stop of  Constrexpr.constr_expr
 
 
@@ -797,8 +794,8 @@ let rec chop_n_arrow n t =
   if n <= 0
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
-    match t with
-      | Constrexpr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
+    match snd t with
+      | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
 					     the remaining number of arrow to chop and [t'] we discard it and
@@ -816,8 +813,8 @@ let rec chop_n_arrow n t =
 		    then
 		      aux (n - nal_l) nal_ta'
 		    else
-		      let new_t' =
-			Constrexpr.CProdN(Loc.ghost,
+		      let new_t' = Loc.tag @@
+			Constrexpr.CProdN(
 					((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
@@ -832,8 +829,8 @@ let rec chop_n_arrow n t =
 
 let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
-  match b with
-    | Constrexpr.CLambdaN (loc, (nal_ta), b') ->
+  match snd b with
+    | Constrexpr.CLambdaN ((nal_ta), b') ->
 	begin
 	  let n =
 	    (List.fold_left (fun n (nal,_,_) ->
@@ -872,8 +869,8 @@ let make_graph (f_ref:global_reference) =
 	 in
 	 let (nal_tas,b,t)  = get_args extern_body extern_type in
 	 let expr_list =
-	   match b with
-	     | Constrexpr.CFix(loc,l_id,fixexprl) ->
+	   match snd b with
+	     | Constrexpr.CFix(l_id,fixexprl) ->
 		 let l =
 		   List.map
 		     (fun (id,(n,recexp),bl,t,b) ->
@@ -885,7 +882,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalDef (na,_,_)-> []
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
-					(fun (loc,n) ->
+					(fun (loc,n) -> Loc.tag ~loc @@ 
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f1ca57585..29de56478 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -73,7 +73,7 @@ let isVarf f x =
     in global environment. *)
 let ident_global_exist id =
   try
-    let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
+    let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.ghost,id), None) in
     let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when CErrors.noncritical e -> false
@@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let c = RelDecl.get_type decl in
         let typ = Constrextern.extern_constr false env Evd.empty c in
         let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
-        CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
+        Loc.tag @@ CProdN ([[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c2..dffd90be3 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -187,7 +187,7 @@ GEXTEND Gram
   (* Tactic arguments to the right of an application *)
   tactic_arg_compat:
     [ [ a = tactic_arg -> a
-      | c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
+      | c = Constr.constr -> (match c with _loc, CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
       (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
@@ -255,10 +255,10 @@ GEXTEND Gram
 	  let t, ty =
 	    match mpv with
 	    | Term t -> (match t with
-	      | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
+	      | _loc, CCast (t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty)
+	  in Def (na, t, Option.default (Term (Loc.tag @@ CHole (None, IntroAnonymous, None))) ty)
     ] ]
   ;
   match_context_rule:
@@ -353,7 +353,7 @@ GEXTEND Gram
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
-          CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
+          Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ]
   ;
   END
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af..1674bb4ca 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -130,14 +130,14 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
           (try List.index Names.Name.equal (snd x) ids
           with Not_found -> error "No such fix variable.")
       | _ -> error "Cannot guess decreasing argument of fix." in
-  (id,n,CProdN(loc,bl,ty))
+  (id,n, Loc.tag ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
     user_err ~loc:aloc
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
-  (id,CProdN(loc,bl,ty))
+  (id,Loc.tag ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
 let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
@@ -154,12 +154,12 @@ let mkTacCase with_evar = function
   (* Reinterpret numbers as a notation for terms *)
   | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
       TacCase (with_evar,
-        (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
+        (clear,(Loc.tag @@ CPrim (Numeral (Bigint.of_int n)),
 	 NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
-      TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings)))
+      TacCase (with_evar,(clear,(Loc.tag @@ CRef (Ident id,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
@@ -169,7 +169,7 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
+      Loc.tag ~loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
   | [] -> c
 
@@ -440,7 +440,7 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+    [ [ na=name -> ([na],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
       | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
     ] ]
   ;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 39ae1f41d..ad76ef9c6 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -340,8 +340,8 @@ type 'a extra_genarg_printer =
 
   let strip_prod_binders_expr n ty =
     let rec strip_ty acc n ty =
-      match ty with
-          Constrexpr.CProdN(_,bll,a) ->
+      match snd ty with
+          Constrexpr.CProdN(bll,a) ->
             let nb =
               List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
             let bll = List.map (fun (x, _, y) -> x, y) bll in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600..1f75f88d4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1787,18 +1787,18 @@ let rec strategy_of_ast = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
+let mkappc s l = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
   (((Loc.ghost,Name n),None), Explicit,
-  CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
+  Loc.tag @@ CAppExpl ((None, Qualid (Loc.ghost, qualid_of_string s),None),
 	   args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
   new_instance (Flags.is_universe_polymorphism ()) 
-    binders instance (Some (true, CRecord (Loc.ghost,fields)))
+    binders instance (Some (true, Loc.tag @@ CRecord (fields)))
     ~global ~generalize:false ~refine:false Hints.empty_hint_info
 
 let declare_instance_refl global binders a aeq n lemma =
@@ -1859,7 +1859,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None)
+let cHole = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None)
 
 let proper_projection sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
@@ -2013,13 +2013,13 @@ let add_morphism glob binders m s n =
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((Loc.ghost,Name instance_id),None), Explicit,
-    CAppExpl (Loc.ghost,
+    Loc.tag @@ CAppExpl (
 	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
     ignore(new_instance ~global:glob poly binders instance 
-	     (Some (true, CRecord (Loc.ghost,[])))
+	     (Some (true, Loc.tag @@ CRecord []))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e..75f890c96 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -110,13 +110,13 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      GVar (dloc,id), Some (CRef (r,None))
+      GVar (dloc,id), Some (Loc.tag @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      GVar (dloc,id), if strict then None else Some (CRef (r,None))
+      GVar (dloc,id), if strict then None else Some (Loc.tag @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       GRef (loc,locate_global_with_alias lqid,None), 
-	if strict then None else Some (CRef (r,None))
+	if strict then None else Some (Loc.tag @@ CRef (r,None))
 
 let intern_move_location ist = function
   | MoveAfter id -> MoveAfter (intern_hyp ist id)
@@ -273,7 +273,7 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	match intern_constr ist (CRef (Ident (dloc,id), None)) with
+	match intern_constr ist (Loc.tag @@ CRef (Ident (dloc,id), None)) with
 	| GVar (loc,id),_ -> clear,ElimOnIdent (loc,id)
 	| c -> clear,ElimOnConstr (c,NoBindings)
       else
@@ -363,7 +363,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
           Inr (bound_names,(c,None),dummy_pat) in
   (l, match p with
   | Inl r -> interp_ref r
-  | Inr (CAppExpl(_,(None,r,None),[])) ->
+  | Inr (_, CAppExpl((None,r,None),[])) ->
       (* We interpret similarly @ref and ref *)
       interp_ref (AN r)
   | Inr c ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 50f43931e..de6c44b2b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1074,7 +1074,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in
+          let c = (GVar (loc,id),Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f3555ebc4..1a5ef825d 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -149,15 +149,15 @@ let add_genarg tag pr =
 (** Constructors for cast type *)
 let dC t = CastConv t
 (** Constructors for constr_expr *)
-let isCVar = function CRef (Ident _, _) -> true | _ -> false
-let destCVar = function CRef (Ident (_, id), _) -> id | _ ->
+let isCVar   = function _loc, CRef (Ident _, _) -> true | _ -> false
+let destCVar = function _loc, CRef (Ident (_, id), _) -> id | _ ->
   CErrors.anomaly (str"not a CRef")
-let mkCHole loc = CHole (loc, None, IntroAnonymous, None)
-let mkCLambda loc name ty t = 
-   CLambdaN (loc, [[loc, name], Default Explicit, ty], t)
-let mkCLetIn loc name bo t = 
-   CLetIn (loc, (loc, name), bo, None, t)
-let mkCCast loc t ty = CCast (loc,t, dC ty)
+let mkCHole loc = Loc.tag ~loc @@ CHole (None, IntroAnonymous, None)
+let mkCLambda loc name ty t = Loc.tag ~loc @@
+   CLambdaN ([[loc, name], Default Explicit, ty], t)
+let mkCLetIn loc name bo t = Loc.tag ~loc @@
+   CLetIn ((loc, name), bo, None, t)
+let mkCCast loc t ty = Loc.tag ~loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
 let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None)
 let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args)
@@ -952,8 +952,8 @@ let glob_cpattern gs p =
   | _, (_, None) as x -> x
   | k, (v, Some t) as orig ->
      if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else
-     match t with
-     | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) ->
+     match snd (Loc.to_pair t) with
+     | CNotation("( _ in _ )", ([t1; t2], [], [])) ->
          (try match glob t1, glob t2 with
          | (r1, None), (r2, None) -> encode k "In" [r1;r2]
          | (r1, Some _), (r2, Some _) when isCVar t1 ->
@@ -961,11 +961,11 @@ let glob_cpattern gs p =
          | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
          | _ -> CErrors.anomaly (str"where are we?")
          with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
-     | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) ->
+     | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [])) ->
          check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
-     | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) ->
+     | CNotation("( _ as _ )", ([t1; t2], [], [])) ->
          encode k "As" [fst (glob t1); fst (glob t2)]
-     | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) ->
+     | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [])) ->
          check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
      | _ -> glob_ssrterm gs orig
 ;;
@@ -1021,8 +1021,8 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern
 
 
 let id_of_cpattern = function
-  | _,(_,Some (CRef (Ident (_, x), _))) -> Some x
-  | _,(_,Some (CAppExpl (_, (_, Ident (_, x), _), []))) -> Some x
+  | _,(_,Some (_loc, CRef (Ident (_, x), _))) -> Some x
+  | _,(_,Some (_loc, CAppExpl ((_, Ident (_, x), _), []))) -> Some x
   | _,(GRef (_, VarRef x, _) ,None) -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
@@ -1378,7 +1378,7 @@ let pf_fill_occ_term gl occ t =
 let cpattern_of_id id = ' ', (GRef (dummy_loc, VarRef  id, None), None)
 
 let is_wildcard = function
-  | _,(_,Some (CHole _)|GHole _,None) -> true
+  | _,(_,Some (_, CHole _)|GHole _,None) -> true
   | _ -> false
 
 (* "ssrpattern" *)