Use more consistent resolution parameters in Program and regular typing

and add an optional fail_evar flag to control resolution better in
interpretation functions.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12197 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 27 insertions, 23 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2aee2ea68f..f3a2b6e0ed 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1243,31 +1243,33 @@ let interp_open_constr_patvar sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
-let interp_constr_evars_gen_impls ?evdref
+let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
     env ?(impls=([],[])) kind c =
-  match evdref with 
-    | None -> 
-	let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
-	let imps = Implicit_quantifiers.implicits_of_rawterm c in
-	  Default.understand_gen kind Evd.empty env c, imps
-    | Some evdref ->
-	let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
-	let imps = Implicit_quantifiers.implicits_of_rawterm c in
-	  Default.understand_tcc_evars evdref env kind c, imps
+  let evdref =
+    match evdref with
+    | None -> ref Evd.empty
+    | Some evdref -> evdref
+  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
+	      
+let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
+    env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
+
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
+
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+  interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
 
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
   let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
     Default.understand_tcc_evars evdref env kind c
-      
-let interp_casted_constr_evars_impls ?evdref
-    env ?(impls=([],[])) c typ =
-  interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
-
-let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
-  interp_constr_evars_gen_impls ?evdref env IsType ~impls c
-
-let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
-  interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
 
 let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 25bcc66b0a..bfccf03d18 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -94,13 +94,15 @@ val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
 
 (* Accepting evars and giving back the manual implicits in addition. *)
 
-val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> 
+val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> 
   ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
 
-val interp_type_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
+  env -> ?impls:full_implicits_env ->
   constr_expr -> types * manual_implicits
 
-val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
+  env -> ?impls:full_implicits_env ->
   constr_expr -> constr * manual_implicits
 
 val interp_casted_constr_evars : evar_defs ref -> env ->