The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I was going to ask the same question. Perhaps an example could help?

On Thu, Oct 15, 2020 at 3:08 AM Fabian Kunze <fabian.kunze AT cs.uni-saarland.de> wrote:

By closed, do you mean no evars, or no local variables?

15 Oct 2020 07:42:39 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

Sorry, I was not clear. I want to only strongly normalize closed subterms of the type and leave the rest unchanged.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Oct 14, 2020 at 6:54 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Sorry, that only does goal, but doing the context isn't much different

On Wed, Oct 14, 2020, 20:53 Jason Gross <jasongross9 AT gmail.com> wrote:

Here is a slow tactic to do this:

Ltac norm T :=

  repeat match goal with

          | [ |- context [?e] ] => let e' := eval vm_compute in (e : T) in progress change e with e'

         end.

You may want a different typing check if you don't want coercion insertion or only want to check up to syntactic typing rather than unification.

On Wed, Oct 14, 2020, 20:20 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a tactic to strongly normalize all closed terms of a given type in the Coq goal and context?

Is there a way to write such a tactic in Ltac/Ltac2/Mtac2.... ?

-- Abhishek

http://www.cs.cornell.edu/~aa755/