Record updating notations

update_record.v

Definition marker {T} (v : T) := v.                                                                                                                                                                         
Ltac apply_with_underscores f x :=                                                                                                                                                                          
  match constr:(Set) with                                                                                                                                                                                   
  | _ => constr:(f x)                                                                                                                                                                                       
  | _ => apply_with_underscores uconstr:(f _) x                                                                                                                                                             
  end.                                                                                                                                                                                                      
Ltac update_record v accessor new_value :=                                                                                                                                                                  
  let T := type of v in                                                                                                                                                                                     
  let v' := open_constr:(ltac:(econstructor) : T) in                                                                                                                                                        
  let accessed := apply_with_underscores accessor v' in                                                                                                                                                     
  let accessed := (eval hnf in accessed) in                                                                                                                                                                 
  let unif := open_constr:(eq_refl : accessed = marker _) in                                                                                                                                                
  let v'' := (eval cbv [marker] in v') in                                                                                                                                                                   
  let unif := constr:(eq_refl : v = v'') in                                                                                                                                                                 
  lazymatch v' with                                                                                                                                                                                         
  | context G[marker _] => let G' := context G[new_value] in                                                                                                                                                
                           G'                                                                                                                                                                               
  end.                                                                                                                                                                                                      
                                                                                                                                                                                                            
Tactic Notation "update!" constr(v) "setting" uconstr(accessor) "to" constr(new_value)                                                                                                                      
  := let res := update_record v accessor new_value in                                                                                                                                                       
     exact res.                                                                                                                                                                                             
                                                                                                                                                                                                            
Set Primitive Projections.                                                                                                                                                                                  
Record prod A B := pair { fst : A ; snd : B }.                                                                                                                                                              
Arguments pair {A B} _ _.                                                                                                                                                                                   
Arguments fst {A B} _.                                                                                                                                                                                      
Arguments snd {A B} _.                                                                                                                                                                                      
                                                                                                                                                                                                            
Notation "'update!' v 'setting' accessor 'to' new_value" := (ltac:(update! v setting accessor to new_value)) (only parsing, at level 90).                                                                   
Check ltac:(update! {| fst := 1 ; snd := 2 |} setting fst to 3).                                                                                                                                            
Check update! {| fst := 1 ; snd := 2 |} setting @fst to 3.