From 5a6723701a3ebf6b01d9611ec64a4d12a9890014 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 2 May 2022 09:56:26 +0200
Subject: [PATCH] [kernel] Ast_diff: fails on Code_annot that should not happen
in normalized AST.
Instead of silently ignoring them and always returning `Same_body.
---
src/kernel_services/ast_queries/ast_diff.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 44c15508964..56025255e45 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1105,7 +1105,7 @@ and is_same_instr i i' env: body_correspondance*is_same_env =
| Skip _, Skip _ -> `Same_body, env
| Code_annot _, Code_annot _ ->
(* should not be present in normalized AST *)
- `Same_body, env
+ Kernel.fatal "Unexpected Code_annot instruction in normalized AST"
| _ -> `Body_changed, env
and is_same_instr_list l l' env =
--
GitLab