From e8cfc6583942e7522bd32aff2bfd6f4b3a972a17 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 26 Feb 2024 14:22:56 +0100 Subject: [PATCH] Don't use vmcast to convert the reified goal and actual goal VM can't avoid computing subterms of the goal that should be left alone. Fix #133 --- src/aac_rewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/aac_rewrite.ml b/src/aac_rewrite.ml index 4d76709..be32bdf 100644 --- a/src/aac_rewrite.ml +++ b/src/aac_rewrite.ml @@ -135,7 +135,7 @@ let by_aac_reflexivity zero (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in - let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast in + let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.DEFAULTcast in let apply_tac = Tactics.apply decision_thm in let open Proofview in Coq.tclRETYPE decision_thm