From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 plugins/quote/quote.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index f0ca3bb9..216a719d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -221,7 +221,10 @@ 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 e when Errors.noncritical e -> 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