From 72324aced4c7f2bc400554a6918755c5b46ece24 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 17 Nov 2014 13:18:44 +0100
Subject: Avoid compilation warning.

---
 pretyping/miscops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 882ebafe11..10129306de 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -56,4 +56,4 @@ let map_red_expr_gen f g h = function
   | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o)
   | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
   | Cbn flags -> Cbn (map_flags g flags)
-  | ExtraRedExpr _ | Red _ | Hnf _ as x -> x
+  | ExtraRedExpr _ | Red _ | Hnf as x -> x
-- 
cgit v1.2.3