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
---
 pretyping/pretyping.ml  | 6 +++---
 pretyping/pretyping.mli | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9f90e53a72..05c27cd342 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -101,7 +101,7 @@ sig
   val understand_tcc : ?resolve_classes:bool ->
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
 
-  val understand_tcc_evars :
+  val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
     evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
     
   (* More general entry point with evars from ltac *)
@@ -724,8 +724,8 @@ module Pretyping_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 = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 974cba1b4d..9b1f57484b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -43,7 +43,7 @@ sig
   val understand_tcc : ?resolve_classes:bool ->
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
     
-  val understand_tcc_evars :
+  val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
     evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
 
   (* More general entry point with evars from ltac *)
-- 
cgit v1.2.3