The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

when I simplify a hypothesis and then apply it, the proof term contains the 
original unsimplified hypothesis:

Require Import List.
Open Scope list_scope.
Import ListNotations.

Definition a := [1;2;3].

Definition x : list nat.
  set (H:= [1;2;3] ++ [4;5;6] ).
  compute in H. 
  exact H.
Defined.

Print x. (* Results in x = let H := [1; 2; 3] ++ [4; 5; 6] in H : list nat *)

This is a bit inconvenient, especially in connection with the new $( )$ 
syntax.
Of cause I can use "Eval compute in" or similar outside of $( )$ but in some 
cases I want to be more selective in how to simplifiy which term. 
I wonder if there is a way to get the simplified proof term in the proof term.

Btw.: "Eval compute in" doesn't work with "Instance", which might be a useful 
feature in connection with $( )$.

Best regards,

Michael