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

4 files changed, 7 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f3a2b6e0ed..d8c4a70678 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1252,10 +1252,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
   in
   let c = intern_gen (kind=IsType) ~impls !evdref env c in
   let imps = Implicit_quantifiers.implicits_of_rawterm c in
-    if fail_evar then 
-      Default.understand_gen kind !evdref env c, imps
-    else
-      Default.understand_tcc_evars evdref env kind c, imps
+    Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
 	      
 let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
     env ?(impls=([],[])) c typ =
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)
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 *)