From 91c1f2827911c29e5d26e72037f7856f2e3e57f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 10 Oct 2024 17:40:13 -0700 Subject: [PATCH] Update manual ml fixup file for new internals --- tests/semiring/CanonCommSemiring.ml.fixup | 34 +++++++++++------------ 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/tests/semiring/CanonCommSemiring.ml.fixup b/tests/semiring/CanonCommSemiring.ml.fixup index e878dced53d..02da1deab67 100644 --- a/tests/semiring/CanonCommSemiring.ml.fixup +++ b/tests/semiring/CanonCommSemiring.ml.fixup @@ -3,7 +3,7 @@ (* This is needed since we have no automatic embeddings for Tac functions, but we should add them *) let _ = - FStar_Tactics_Native.register_tactic "CanonCommSemiring.canon_semiring_aux" + FStarC_Tactics_Native.register_tactic "CanonCommSemiring.canon_semiring_aux" (Prims.parse_int "11") (fun psc -> fun ncb -> @@ -11,22 +11,22 @@ let _ = fun args -> match args with | (tv_0,_)::args_tail -> - (FStar_Tactics_InterpFuns.mk_tactic_interpretation_9 + (FStarC_Tactics_InterpFuns.mk_tactic_interpretation_9 "CanonCommSemiring.canon_semiring_aux (plugin)" - (FStar_Tactics_Native.from_tactic_9 canon_semiring_aux) - FStar_Reflection_V2_Embeddings.e_term - (FStar_Tactics_Interpreter.e_tactic_1_alt - FStar_Reflection_V2_Embeddings.e_term - (FStar_Syntax_Embeddings.mk_any_emb tv_0)) - (FStar_Tactics_Interpreter.e_tactic_1_alt - (FStar_Syntax_Embeddings.mk_any_emb tv_0) - FStar_Reflection_V2_Embeddings.e_term) - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term - FStar_Syntax_Embeddings.e_any - FStar_Syntax_Embeddings.e_unit + (FStarC_Tactics_Native.from_tactic_9 canon_semiring_aux) + FStarC_Reflection_V2_Embeddings.e_term + (FStarC_Tactics_Interpreter.e_tactic_1_alt + FStarC_Reflection_V2_Embeddings.e_term + (FStarC_Syntax_Embeddings.mk_any_emb tv_0)) + (FStarC_Tactics_Interpreter.e_tactic_1_alt + (FStarC_Syntax_Embeddings.mk_any_emb tv_0) + FStarC_Reflection_V2_Embeddings.e_term) + FStarC_Reflection_V2_Embeddings.e_term + FStarC_Reflection_V2_Embeddings.e_term + FStarC_Reflection_V2_Embeddings.e_term + FStarC_Reflection_V2_Embeddings.e_term + FStarC_Reflection_V2_Embeddings.e_term + FStarC_Syntax_Embeddings.e_any + FStarC_Syntax_Embeddings.e_unit psc ncb us) args_tail | _ -> failwith "arity mismatch")