The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

This should be what you are after:

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

On 2 February 2015 at 10:54, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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