From 604a07a7d425aa4b89bcd391c083d8600c71c5b5 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 22 Jun 2009 18:28:18 +0000
Subject: Fixes for r12197, the refined evars were not returned in case
 fail_evar was true.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_pretyping_F.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 8456d24a99..a1d9603187 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -629,8 +629,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
     ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
 
-  let understand_tcc_evars evdref env kind c =
-    pretype_gen false true evdref env ([],[]) kind c
+  let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
+    pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
 end
 
 module Default : S = SubtacPretyping_F(Coercion.Default)
-- 
cgit v1.2.3