From aa8fa58d617bd68876338cf70a03d700283fed74 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 10 Apr 2024 13:38:44 +0200 Subject: [PATCH] Replace calls to "vm_compute in hyps" by plain calls to vm_compute. The terms are of type "Internal.T env_sym", so invoking "vm_compute in" on them ends up strongly normalizing the function env_sym, which explodes. By using "eval vm_compute" instead, only the bodies get strongly normalized. --- theories/AAC.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/theories/AAC.v b/theories/AAC.v index 7298663..6e6a4cc 100644 --- a/theories/AAC.v +++ b/theories/AAC.v @@ -936,7 +936,9 @@ End Internal. Local Ltac internal_normalize := let x := fresh in let y := fresh in - intro x; intro y; vm_compute in x; vm_compute in y; unfold x; unfold y; + intro x; intro y; + let vx := eval vm_compute in x in change x with vx; + let vy := eval vm_compute in y in change y with vy; compute [Internal.eval Utils.fold_map Internal.copy Prect]; simpl. (** ** Lemmas for performing transitivity steps given an AAC_lift instance *)