From 552df1605233769ad3cdabaadaa0011605e79797 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Mar 2013 00:00:12 +0000
Subject: Restrict (try...with...) to avoid catching critical exn (part 7)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2c41b95f30..60ae0784fc 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -220,7 +220,7 @@ let compute_rhs bodyi index_of_f =
 (*s Now the function [compute_ivs] itself *)
 
 let compute_ivs gl f cs =
-  let cst = try destConst f with _ -> i_can't_do_that () in
+  let cst = try destConst f with DestKO -> i_can't_do_that () in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
-- 
cgit v1.2.3