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

6 files changed, 34 insertions, 28 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 -> 
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index f16fa1c7a6..91418e05e7 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -74,6 +74,7 @@ let interp env isevars c tycon =
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
   let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
   let evm =  unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 23d8457327..8456d24a99 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -580,7 +580,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     evdref := fst (consider_remaining_unif_problems env !evdref);
     if resolve_classes then
       evdref := 
-        Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref;
+        Typeclasses.resolve_typeclasses ~onlyargs:false
+	  ~split:true ~fail:fail_evar env !evdref;
     let c = nf_evar !evdref c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 91cdff5fb4..9f90e53a72 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -672,8 +672,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     evdref := fst (consider_remaining_unif_problems env !evdref);
     if resolve_classes then
       evdref := 
-        Typeclasses.resolve_typeclasses ~onlyargs:(not fail_evar)
-	  ~split:false ~fail:fail_evar env !evdref;
+        Typeclasses.resolve_typeclasses ~onlyargs:false
+	  ~split:true ~fail:fail_evar env !evdref;
     let c = nf_evar !evdref c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d2eed98e45..910a2526af 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -105,8 +105,8 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
 	let ty = generalize_constr_expr comtyp bl in
 	let b = abstract_constr_expr com bl in
 	let evdref = ref Evd.empty in
-	let ty, impls = interp_type_evars_impls ~evdref env ty in
-	let b, imps = interp_casted_constr_evars_impls ~evdref env b ty in
+	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env ty in
+	let b, imps = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env b ty in
 	let body, typ = nf_isevar !evdref b, nf_isevar !evdref ty in
 	  check_evars env Evd.empty !evdref body;
 	  check_evars env Evd.empty !evdref typ;