From f3ef82fee78d40c628d319dab4cc35a41c638e8e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 23 Jul 2018 16:14:12 +0100
Subject: Coq: make all pattern matches in the output exhaustive Uses previous
 stage to deal with (e.g.) guards. New option -dcoq_warn_nonex tells you where
 all of the extra default cases were added.

---
 src/process_file.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/process_file.ml')

diff --git a/src/process_file.ml b/src/process_file.ml
index 9ed52e8d..c3e1b510 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -398,7 +398,7 @@ let rewrite rewriters defs =
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
 let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined bitvectors x)]
 let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
-let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_lem
+let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq
 let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
 let rewrite_ast_c ast =
   ast
-- 
cgit v1.2.3