A uniformization step around understand_* and interp_* functions.

- Clarification of the existence of three algorithms for solving
  unconstrained evars:
  - the type-class mechanism
  - the heuristics for solving pending conversion problems and multi-candidates
  - Declare Implicit Tactic (when called from tactics)

  Main function for solving unconstrained evars (when not using
  understand): Pretyping.solve_remaining_evars

- Clarification of the existence of three corresponding kinds of
  errors when reporting about unsolved evars:

  Main function for checking resolution of evars independently of the
  understand functions: Pretyping.check_evars_are_solved

- Introduction of inference flags in pretyping for governing which
  combination of the algorithms to use when calling some understand
  function; there is also a flag of expanding or not evars and for
  requiring or not the resolution of all evars

- Less hackish way of managing Pretyping.type_constraint: all three
  different possibilities are now represented by three different
  constructors

- Main semantical changes done:
  - solving unconstrained evars and reporting is not any longer mixed:
    one first tries to find unconstrained evars by any way possible;
    one eventually reports on the existence of unsolved evars using
    check_evars_are_solved
  - checking unsolved evars is now done by looking at the evar map,
    not by looking at the evars occurring in the terms to pretype; the
    only observed consequence so far is in Cases.v because of subterms
    (surprisingly) disappering after compilation of pattern-matching
  - the API changed, see dev/doc/changes.txt

Still to do:

- Find more uniform naming schemes:
  - for distinguishing when sigma is passed as a reference or as a value
    (are used: suffix _evars, prefix e_)
  - for distinguishing when evars are allowed to remain uninstantiated or not
    (are used: suffix _evars, again, suffix _tcc, infix _open_)
  - be more consistent on the use of names evd/sigma/evars or evdref/evars
- By the way, shouldn't "understand" be better renamed into "infer" or
  "preinfer", or "pretype". Grammatically, "understanding a term" looks
  strange.
- Investigate whether the inference flags in tacinterp.ml are really
  what we want (e.g. do we really want that heuristic remains
  activated when typeclasses are explicitly deactivated, idem in
  Tacinterp.interp_open_constr where flags are strange).

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

26 files changed, 385 insertions, 317 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index fd3c2e19a1..2164830a7c 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -55,6 +55,25 @@
   * move_location (now in Misctypes) has two new constructors
     MoveFirst and MoveLast replacing (MoveToEnd false) and (MoveToEnd true)
 
+- API of pretyping.ml and constrintern.ml has been made more uniform
+  * Parametrization of understand_* functions is now made using
+    "inference flags"
+  * Functions removed:
+    - interp_constr_judgment (inline its former body if really needed)
+    - interp_casted_constr, interp_type: use instead interp_constr with
+      expected_type set to OfType or to IsType
+    - interp_gen: use any of interp_constr, interp_casted_constr, interp_type
+    - interp_open_constr_patvar
+    - interp_context: use interp_context_evars (with a "evar_map ref") and
+      call solve_remaining_evars afterwards with a failing flag
+      (e.g. all_and_fail_flags)
+    - understand_type, understand_gen: use understand with appropriate
+      parameters
+  * Change of semantics:
+    - Functions interp_*_evars_impls have a different interface and do
+      not any longer check resolution of evars by default; use
+      check_evars_are_solved explicitly to check that evars are solved.
+  See also the corresponding commit log.
 
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 339a01d973..6eed1d0ed3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,8 +1659,8 @@ let extract_ids env =
 
 let scope_of_type_kind = function
   | IsType -> Some Notation.type_scope
-  | OfType (Some typ) -> compute_type_scope typ
-  | OfType None -> None
+  | OfType typ -> compute_type_scope typ
+  | WithoutTypeConstraint -> None
 
 let intern_gen kind sigma env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
@@ -1671,7 +1671,7 @@ let intern_gen kind sigma env
 			 impls = impls}
     allow_patvar (ltacvars, []) c
 
-let intern_constr sigma env c = intern_gen (OfType None) sigma env c
+let intern_constr sigma env c = intern_gen WithoutTypeConstraint sigma env c
 
 let intern_type sigma env c = intern_gen IsType sigma env c
 
@@ -1688,81 +1688,64 @@ let intern_pattern globalenv patt =
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
-let interp_gen kind sigma env
-               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
-               c =
-  let c = intern_gen kind ~impls ~allow_patvar ~ltacvars sigma env c in
-    understand_gen kind sigma env c
+(* All evars resolved *)
+
+let interp_gen kind sigma env ?(impls=empty_internalization_env) c =
+  let c = intern_gen kind ~impls sigma env c in
+  understand ~expected_type:kind sigma env c
 
-let interp_constr sigma env c =
-  interp_gen (OfType None) sigma env c
+let interp_constr sigma env ?(impls=empty_internalization_env) c =
+  interp_gen WithoutTypeConstraint sigma env c
 
 let interp_type sigma env ?(impls=empty_internalization_env) c =
   interp_gen IsType sigma env ~impls c
 
 let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
-  interp_gen (OfType (Some typ)) sigma env ~impls c
+  interp_gen (OfType typ) sigma env ~impls c
+
+(* Not all evars expected to be resolved *)
 
 let interp_open_constr sigma env c =
   understand_tcc sigma env (intern_constr sigma env c)
 
-let interp_open_constr_patvar sigma env c =
-  let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in
-  let sigma = ref sigma in
-  let evars = ref (Id.Map.empty : glob_constr Id.Map.t) in
-  let rec patvar_to_evar r = match r with
-    | GPatVar (loc,(_,id)) ->
-	( try Id.Map.find id !evars
-	  with Not_found ->
-	    let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
-	    let ev = Evarutil.e_new_evar sigma env ev in
-	    let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
-	    evars := Id.Map.add id rev !evars;
-	    rev
-	)
-    | _ -> map_glob_constr patvar_to_evar r in
-  let raw = patvar_to_evar raw in
-    understand_tcc !sigma env raw
-
-let interp_constr_judgment sigma env c =
-  understand_judgment sigma env (intern_constr sigma env c)
-
-let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
-    env ?(impls=empty_internalization_env) kind c =
-  let evdref =
-    match evdref with
-    | None -> ref Evd.empty
-    | Some evdref -> evdref
-  in
-  let istype = kind == IsType in
-  let c = intern_gen kind ~impls !evdref env c in
-  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
-    understand_tcc_evars ~fail_evar evdref env kind c, imps
+(* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
-    env ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
+let interp_constr_evars_gen_impls evdref
+    env ?(impls=empty_internalization_env) expected_type c =
+  let c = intern_gen expected_type ~impls !evdref env c in
+  let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
+    understand_tcc_evars evdref env ~expected_type c, imps
 
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
+let interp_constr_evars_impls evdref env ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls evdref env ~impls WithoutTypeConstraint c
 
-let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
+let interp_casted_constr_evars_impls evdref env ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen_impls evdref env ~impls (OfType typ) c
 
-let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c =
-  let c = intern_gen kind ~impls !evdref env c in
-    understand_tcc_evars evdref env kind c
+let interp_type_evars_impls evdref env ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls evdref env ~impls IsType c
+
+(* Not all evars expected to be resolved, with side-effect on evars *)
+
+let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) expected_type c =
+  let c = intern_gen expected_type ~impls !evdref env c in
+  understand_tcc_evars evdref env ~expected_type c
+
+let interp_constr_evars evdref env ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen evdref env WithoutTypeConstraint ~impls c
 
 let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
+  interp_constr_evars_gen evdref env ~impls (OfType typ) c
 
 let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
+(* Miscellaneous *)
+
 type ltac_sign = Id.t list * unbound_ltac_var_map
 
 let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
-  let c = intern_gen (if as_type then IsType else OfType None)
+  let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
             ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_glob_constr c
 
@@ -1787,37 +1770,38 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
 let interp_binder sigma env na t =
   let t = intern_gen IsType sigma env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-  understand_type sigma env t'
+  understand ~expected_type:IsType sigma env t'
 
 let interp_binder_evars evdref env na t =
   let t = intern_gen IsType !evdref env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-  understand_tcc_evars evdref env IsType t'
+  understand_tcc_evars evdref env ~expected_type:IsType t'
 
 open Environ
 
 let my_intern_constr sigma env lvar acc c =
   internalize sigma env acc false lvar c
 
-let intern_context global_level sigma env impl_env params =
+let intern_context global_level sigma env impl_env binders =
   try
   let lvar = (([],[]), []) in
   let lenv, bl = List.fold_left
 	    (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar)
 	    ({ids = extract_ids env; unb = false;
-	      tmp_scope = None; scopes = []; impls = impl_env}, []) params in
+	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map snd bl)
   with InternalizationError (loc,e) ->
     user_err_loc (loc,"internalize", explain_internalization_error e)
 
-let interp_rawcontext_gen understand_type understand_judgment env bl =
+let interp_rawcontext_evars evdref env bl =
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
 	match b with
 	    None ->
 	      let t' = locate_if_isevar (loc_of_glob_constr t) na t in
-	      let t = understand_type env t' in
+	      let t =
+                understand_tcc_evars evdref env ~expected_type:IsType t' in
 	      let d = (na,None,t) in
 	      let impls =
 		if k == Implicit then
@@ -1827,21 +1811,14 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
 	      in
 		(push_rel d env, d::params, succ n, impls)
 	  | Some b ->
-	      let c = understand_judgment env b in
+	      let c = understand_judgment_tcc evdref env b in
 	      let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in
 		(push_rel d env, d::params, succ n, impls))
       (env,[],1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
-  let int_env,bl = intern_context global_level sigma env impl_env params in
-    int_env, interp_rawcontext_gen understand_type understand_judgment env bl
-
-let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
-  interp_context_gen (understand_type sigma)
-    (understand_judgment sigma) ~global_level ~impl_env sigma env params
-
 let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
-  interp_context_gen (fun env t -> understand_tcc_evars evdref env IsType t)
-    (understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params
+  let int_env,bl = intern_context global_level !evdref env impl_env params in
+  let x = interp_rawcontext_evars evdref env bl in
+  int_env, x
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index e352c7f7a3..32e878165c 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,51 +88,47 @@ val intern_pattern : env -> cases_pattern_expr ->
 
 val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
-(** {6 Composing internalization with pretyping } *)
+(** {6 Composing internalization with type inference (pretyping) } *)
 
-(** Main interpretation function *)
+(** Main interpretation functions expecting evars to be all resolved *)
 
-val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+val interp_constr : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> constr
 
-(** Particular instances *)
-
-val interp_constr : evar_map -> env ->
-  constr_expr -> constr
+val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
+  constr_expr -> types -> constr
 
 val interp_type : evar_map -> env -> ?impls:internalization_env ->
   constr_expr -> types
 
-val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
-
-val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
-
-val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
-  constr_expr -> types -> constr
+(** Main interpretation function expecting evars to be all resolved *)
 
-(** Accepting evars and giving back the manual implicits in addition. *)
-
-val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
-  ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits
+val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
-val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:internalization_env ->
-  constr_expr -> types * Impargs.manual_implicits
+(** Accepting unresolved evars *)
 
-val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
-  env -> ?impls:internalization_env ->
-  constr_expr -> constr * Impargs.manual_implicits
+val interp_constr_evars : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr -> constr
 
 val interp_casted_constr_evars : evar_map ref -> env ->
   ?impls:internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
-  constr_expr -> types
+val interp_type_evars : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr -> types
+
+(** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-(** {6 Build a judgment  } *)
+val interp_constr_evars_impls : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr ->
+  constr * Impargs.manual_implicits
 
-val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+val interp_casted_constr_evars_impls : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr -> types ->
+  constr * Impargs.manual_implicits
+
+val interp_type_evars_impls : evar_map ref -> env ->
+  ?impls:internalization_env -> constr_expr ->
+  types * Impargs.manual_implicits
 
 (** Interprets constr patterns *)
 
@@ -154,16 +150,10 @@ val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types
 
 (** Interpret contexts: returns extended env and context *)
 
-val interp_context_gen : (env -> glob_constr -> types) ->
-  (env -> glob_constr -> unsafe_judgment) ->
+val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-  
-val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-
-val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
-  evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+  evar_map ref -> env -> local_binder list ->
+  internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index b9334801cd..c4d6a7a304 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -150,7 +150,7 @@ let interp_justification_items sigma env =
 
 let interp_constr check_sort sigma env c =
   if check_sort then
-    understand_type sigma env (fst c)
+    understand sigma env ~expected_type:IsType (fst c)
   else
     understand sigma env (fst c)
 
@@ -175,7 +175,7 @@ let get_eq_typ info env =
     typ
 
 let interp_constr_in_type typ sigma env c =
-  understand sigma env (fst c) ~expected_type:typ
+  understand sigma env (fst c) ~expected_type:(OfType typ)
 
 let interp_statement interp_it sigma env st =
   {st_label=st.st_label;
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 5e55bcfb27..70c7f8d1fa 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1280,7 +1280,7 @@ let understand_my_constr c gls =
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand)
     | rc ->  map_glob_constr frob rc
   in
-  Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc)
+  Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc)
 
 let my_refine c gls =
   let oc = understand_my_constr c gls in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e98a0952b9..e1de8be82a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -334,7 +334,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
     | Anonymous -> env
     | Name id ->
 	let value = Option.map (Pretyping.understand Evd.empty env) raw_value in
-	let typ = Pretyping.understand_type Evd.empty env raw_typ in
+	let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
 	Environ.push_named (id,value,typ) env
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index fcd1c5360e..2a0bbd7b78 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function
         (abstract_glob_constr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
-  Constrintern.intern_gen (Pretyping.OfType None) sigma env ~impls
+  Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 (*
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 34085dca2f..4b9704c2c9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1449,7 +1449,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let equation_lemma_type = 
     nf_betaiotazeta
-      (interp_gen (OfType None) Evd.empty env ~impls:rec_impls eq) 
+      (interp_constr Evd.empty env ~impls:rec_impls eq)
   in
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f859d0b421..24cc7aef80 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -837,7 +837,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
 
-let check_problems_are_solved env evd =
+let check_problems_are_solved evd =
   match snd (extract_all_conv_pbs evd) with
   | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
   | _ -> ()
@@ -915,7 +915,7 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = aux evd pbs false [] in
-  check_problems_are_solved env heuristic_solved_evd;
+  check_problems_are_solved heuristic_solved_evd;
   solve_unconstrained_impossible_cases heuristic_solved_evd
 
 (* Main entry points *)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 655dc1c1a2..c4961873a0 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -37,6 +37,11 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -
 
 val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
 
+(** Check all pending unification problems are solved and raise an
+    error otherwise *)
+
+val check_problems_are_solved : evar_map -> unit
+
 (** Check if a canonical structure is applicable *)
 
 val check_conv_record : constr * types stack -> constr * types stack ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6253fcfbfb..0af88d1dc3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,7 +44,7 @@ open Evarconv
 open Pattern
 open Misctypes
 
-type typing_constraint = OfType of types option | IsType
+type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = (Id.t * constr_under_binders) list
 type unbound_ltac_var_map = (Id.t * Id.t option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
@@ -103,46 +103,78 @@ let interp_elimination_sort = function
   | GSet  -> InSet
   | GType _ -> InType
 
-let resolve_evars env evdref fail_evar resolve_classes =
-  if resolve_classes then
-    (evdref := Typeclasses.resolve_typeclasses 
+type inference_flags = {
+  use_typeclasses : bool;
+  use_unif_heuristics : bool;
+  use_hook : (env -> evar_map -> evar -> constr) option;
+  fail_evar : bool;
+  expand_evars : bool
+}
+
+let apply_typeclasses env evdref fail_evar =
+  evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
 	      then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals)
      ~split:true ~fail:fail_evar env !evdref;
-     if Flags.is_program_mode () then (* Try optionally solving the obligations *)
-       evdref := Typeclasses.resolve_typeclasses 
-       ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref;     
-    );
+  if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+    evdref := Typeclasses.resolve_typeclasses
+      ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref
+
+let apply_inference_hook hook initial_sigma evdref =
+  evdref := fold_undefined (fun evk evi sigma ->
+    if not (Evd.mem initial_sigma evk) &&
+      is_undefined sigma evk (* i.e. not defined by side-effect *)
+    then
+      try
+        let c = hook sigma evk in
+        Evd.define evk c sigma
+      with Exit ->
+        sigma
+    else
+      sigma) !evdref !evdref
+
+let apply_heuristics env evdref fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
-  evdref :=
-    (try consider_remaining_unif_problems
-	   ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
-     with e when Errors.noncritical e ->
-       let e = Errors.push e in if fail_evar then raise e else !evdref)
-
-let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
-  let evdref = ref evd in
-  resolve_evars env evdref fail_evar use_classes;
-  let rec proc_rec c =
-    let c = Reductionops.whd_evar !evdref c in
-    match kind_of_term c with
-    | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
-        let sigma = !evdref in
-	(try
-	   let c = hook env sigma ev in
-	   evdref := Evd.define evk c !evdref;
-	   c
-	 with Exit ->
-           if fail_evar then
-	     let evi = Evd.find_undefined sigma evk in
-             let (loc,src) = evar_source evk !evdref in
-	     Pretype_errors.error_unsolvable_implicit loc env sigma evi src None
-           else
-             c)
-    | _ -> map_constr proc_rec c in
-  let c = proc_rec c in
-  (* Side-effect *)
-  !evdref,c
+  try evdref := consider_remaining_unif_problems
+	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in if fail_evar then raise e
+
+let check_typeclasses_instances_are_solved env sigma =
+  (* Naive way, call resolution again with failure flag *)
+  apply_typeclasses env (ref sigma) true
+
+let check_extra_evars_are_solved env initial_sigma sigma =
+  Evd.fold_undefined
+    (fun evk evi () ->
+      if not (Evd.mem initial_sigma evk) then
+        let (loc,k) = evar_source evk sigma in
+	match k with
+	| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+	| _ ->
+	    let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
+	    error_unsolvable_implicit loc env sigma evi k None) sigma ()
+
+let check_evars_are_solved env initial_sigma sigma =
+  check_typeclasses_instances_are_solved env sigma;
+  check_problems_are_solved sigma;
+  check_extra_evars_are_solved env initial_sigma sigma
+
+(* Try typeclasses, hooks, unification heuristics ... *)
+
+let solve_remaining_evars flags env initial_sigma sigma =
+  let evdref = ref sigma in
+  if flags.use_typeclasses then apply_typeclasses env evdref false;
+  if Option.has_some flags.use_hook then
+    apply_inference_hook (Option.get flags.use_hook env) initial_sigma evdref;
+  if flags.use_unif_heuristics then apply_heuristics env evdref false;
+  if flags.fail_evar then check_evars_are_solved env initial_sigma !evdref;
+  !evdref
+
+let process_inference_flags flags env initial_sigma (sigma,c) =
+  let sigma = solve_remaining_evars flags env initial_sigma sigma in
+  let c = if flags.expand_evars then nf_evar sigma c else c in
+  sigma,c
 
 (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
@@ -717,62 +749,72 @@ and pretype_type valcon env evdref lvar = function
 	      error_unexpected_type_loc
                 (loc_of_glob_constr c) env !evdref tj.utj_val v
 
-let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
+let ise_pretype_gen flags sigma env lvar kind c =
+  let evdref = ref sigma in
   let c' = match kind with
+    | WithoutTypeConstraint ->
+        (pretype empty_tycon env evdref lvar c).uj_val
     | OfType exptyp ->
-	let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-	  (pretype tycon env evdref lvar c).uj_val
+	(pretype (mk_tycon exptyp) env evdref lvar c).uj_val
     | IsType ->
 	(pretype_type empty_valcon env evdref lvar c).utj_val 
   in
-    resolve_evars env evdref fail_evar resolve_classes;
-    let c = if expand_evar then nf_evar !evdref c' else c' in
-      if fail_evar then check_evars env Evd.empty !evdref c;
-      c
+  process_inference_flags flags env sigma (!evdref,c')
 
 (* TODO: comment faire remonter l'information si le typage a resolu des
    variables du sigma original. il faudrait que la fonction de typage
    retourne aussi le nouveau sigma...
 *)
 
+let default_inference_flags fail = {
+  use_typeclasses = true;
+  use_unif_heuristics = true;
+  use_hook = None;
+  fail_evar = fail;
+  expand_evars = true }
+
+let no_classes_no_fail_inference_flags = {
+  use_typeclasses = false;
+  use_unif_heuristics = true;
+  use_hook = None;
+  fail_evar = false;
+  expand_evars = true }
+
+let all_and_fail_flags = default_inference_flags true
+let all_no_fail_flags = default_inference_flags false
+
+let on_judgment f j =
+  let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
+  let (c,_,t) = destCast (f c) in
+  {uj_val = c; uj_type = t}
+
 let understand_judgment sigma env c =
   let evdref = ref sigma in
   let j = pretype empty_tycon env evdref ([],[]) c in
-    resolve_evars env evdref true true;
-    let j = j_nf_evar !evdref j in
-      check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-      j
+  on_judgment (fun c ->
+    snd (process_inference_flags all_and_fail_flags env sigma (!evdref,c))) j
 
 let understand_judgment_tcc evdref env c =
   let j = pretype empty_tycon env evdref ([],[]) c in
-    resolve_evars env evdref false true;
-    j_nf_evar !evdref j
-
-(* Raw calls to the unsafe inference machine: boolean says if we must
-   fail on unresolved evars; the unsafe_judgment list allows us to
-   extend env with some bindings *)
-
-let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
-  let evdref = ref sigma in
-  let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
-    !evdref, c
+  on_judgment (fun c ->
+    let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
+    evdref := evd; c) j
 
 (** Entry points of the high-level type synthesis algorithm *)
 
-let understand_gen kind sigma env c =
-  snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
-
-let understand sigma env ?expected_type:exptyp c =
-  snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
-
-let understand_type sigma env c =
-  snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
+let understand
+    ?(flags=all_and_fail_flags)
+    ?(expected_type=WithoutTypeConstraint)
+    sigma env c =
+  snd (ise_pretype_gen flags sigma env ([],[]) expected_type c)
 
-let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c =
-  ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c
+let understand_tcc ?(flags=all_no_fail_flags) sigma env ?(expected_type=WithoutTypeConstraint) c =
+  ise_pretype_gen flags sigma env ([],[]) expected_type c
 
-let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-  ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
+let understand_tcc_evars ?(flags=all_no_fail_flags) evdref env ?(expected_type=WithoutTypeConstraint) c =
+  let sigma, c = ise_pretype_gen flags !evdref env ([],[]) expected_type c in
+  evdref := sigma;
+  c
 
-let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-  pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
+let understand_ltac flags sigma env lvar kind c =
+  ise_pretype_gen flags sigma env lvar kind c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 04d29ac28d..df65f10f33 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -26,7 +26,7 @@ open Misctypes
 val search_guard :
   Loc.t -> env -> int list list -> rec_declaration -> int array
 
-type typing_constraint = OfType of types option | IsType
+type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 type var_map = (Id.t * Pattern.constr_under_binders) list
 type unbound_ltac_var_map = (Id.t * Id.t option) list
@@ -34,6 +34,22 @@ type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
+type inference_flags = {
+  use_typeclasses : bool;
+  use_unif_heuristics : bool;
+  use_hook : (env -> evar_map -> evar -> constr) option;
+  fail_evar : bool;
+  expand_evars : bool
+}
+
+val default_inference_flags : bool -> inference_flags
+
+val no_classes_no_fail_inference_flags : inference_flags
+
+val all_no_fail_flags : inference_flags
+
+val all_and_fail_flags : inference_flags
+
 (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
@@ -41,42 +57,32 @@ val allow_anonymous_refs : bool ref
     unresolved holes as evars and returning the typing contexts of
     these evars. Work as [understand_gen] for the rest. *)
 
-val understand_tcc : ?resolve_classes:bool ->
-  evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
+val understand_tcc : ?flags:inference_flags -> evar_map -> env ->
+  ?expected_type:typing_constraint -> glob_constr -> open_constr
 
-val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-  evar_map ref -> env -> typing_constraint -> glob_constr -> constr
+val understand_tcc_evars : ?flags:inference_flags -> evar_map ref -> env ->
+  ?expected_type:typing_constraint -> glob_constr -> constr
 
 (** More general entry point with evars from ltac *)
 
-(** Generic call to the interpreter from glob_constr to constr, failing
-    unresolved holes in the glob_constr cannot be instantiated.
+(** Generic call to the interpreter from glob_constr to constr
 
-    In [understand_ltac expand_evars sigma env ltac_env constraint c],
+    In [understand_ltac flags sigma env ltac_env constraint c],
 
-    expand_evars : expand inferred evars by their value if any
-    sigma : initial set of existential variables (typically dependent subgoals)
-    ltac_env : partial substitution of variables (used for the tactic language)
-    constraint : tell if interpreted as a possibly constrained term or a type
+    flags: tell how to manage evars
+    sigma: initial set of existential variables (typically current goals)
+    ltac_env: partial substitution of variables (used for the tactic language)
+    constraint: tell if interpreted as a possibly constrained term or a type
 *)
 
-val understand_ltac : ?resolve_classes:bool ->
-  bool -> evar_map -> env -> ltac_var_map ->
+val understand_ltac : inference_flags ->
+  evar_map -> env -> ltac_var_map ->
   typing_constraint -> glob_constr -> pure_open_constr
 
 (** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
-val understand : evar_map -> env -> ?expected_type:Term.types ->
-  glob_constr -> constr
-
-(** Idem but the glob_constr is intended to be a type *)
-
-val understand_type : evar_map -> env -> glob_constr -> constr
-
-(** A generalization of the two previous case *)
-
-val understand_gen : typing_constraint -> evar_map -> env ->
-  glob_constr -> constr
+val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
+  evar_map -> env -> glob_constr -> constr
 
 (** Idem but returns the judgment of the understood term *)
 
@@ -85,6 +91,17 @@ val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
 (** Idem but do not fail on unresolved evars *)
 val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
 
+(** Trying to solve remaining evars and remaining conversion problems
+    with type classes, heuristics, and possibly an external solver *)
+
+val solve_remaining_evars : inference_flags ->
+  env -> (* initial map *) evar_map -> (* map to solve *) evar_map -> evar_map
+
+(** Checking evars are all solved and reporting an appropriate error message *)
+
+val check_evars_are_solved :
+  env -> (* initial map: *) evar_map -> (* map to check: *) evar_map -> unit
+
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
@@ -95,9 +112,9 @@ val pretype_type :
   val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
-val pretype_gen :
-  bool -> bool -> bool -> evar_map ref -> env ->
-  ltac_var_map -> typing_constraint -> glob_constr -> constr
+val ise_pretype_gen :
+  inference_flags -> evar_map -> env ->
+  ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
 
 (**/**)
 
@@ -108,8 +125,3 @@ val constr_out : Dyn.t -> constr
 
 val interp_sort : glob_sort -> sorts
 val interp_elimination_sort : glob_sort -> sorts_family
-
-(** Last chance for solving evars, possibly using external solver *)
-val solve_remaining_evars : bool -> bool ->
-  (env -> evar_map -> existential -> constr) ->
-  env -> evar_map -> pure_open_constr -> pure_open_constr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fff4f67b12..0e317e68e5 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -41,8 +41,14 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     error "Instantiate called on already-defined evar";
   let env = Evd.evar_filtered_env evi in
   let sigma',typed_c =
-    try Pretyping.understand_ltac ~resolve_classes:true true 
-      sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc
+    let flags = {
+      Pretyping.use_typeclasses = true;
+      Pretyping.use_unif_heuristics = true;
+      Pretyping.use_hook = None;
+      Pretyping.fail_evar = false;
+      Pretyping.expand_evars = true } in
+    try Pretyping.understand_ltac flags
+      sigma env ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when Errors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6b794c1479..67cd414125 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -111,9 +111,7 @@ let return v _ _ _ _ = v
     In an ideal world, this could/should be the other way round.
     As of now, though, it seems at least quite useful to build tactics. *)
 let interp_constr cexpr env rdefs _ _ =
-  let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in
-  rdefs := defs ;
-  c
+  Constrintern.interp_constr_evars rdefs env cexpr
 
 (* Type of constr with holes used by refine. *)
 (* The list of evars doesn't necessarily contain all the evars in the constr,
@@ -217,11 +215,14 @@ module Refinable = struct
     let init_defs = !rdefs in
     (* if [check_type] is true, then creates a type constraint for the
        proof-to-be *)
-    let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in
+    let tycon = if check_type then Pretyping.OfType (Evd.evar_concl info) else Pretyping.WithoutTypeConstraint in
     (* call to [understand_tcc_evars] returns a constr with undefined evars
        these evars will be our new goals *)
+    let flags =
+      if resolve_classes then Pretyping.all_no_fail_flags
+      else Pretyping.no_classes_no_fail_inference_flags in
     let open_constr =
-      Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
+      Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc
     in
       ignore(update_handle handle init_defs !rdefs);
       open_constr
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c07db32b75..90f20a7385 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -171,7 +171,7 @@ let implicit_tactic = ref None
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
 
-let solve_by_implicit_tactic env sigma (evk,args) =
+let solve_by_implicit_tactic env sigma evk =
   let evi = Evd.find_undefined sigma evk in
   match (!implicit_tactic, snd (evar_source evk sigma)) with
   | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4ca23e7116..73850c6f07 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -174,4 +174,4 @@ val build_by_tactic : env -> types -> tactic -> constr
 val declare_implicit_tactic : tactic -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr
+val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d1abdd0af4..9ae7775caf 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -342,7 +342,7 @@ let intern_binding_name ist x =
 
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
-  let scope = if isarity then Pretyping.IsType else Pretyping.OfType None in
+  let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 08de6cb027..da0a3c7d9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -465,7 +465,7 @@ let interp_fresh_id ist env l =
 
 let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
 
-let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) =
+let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
   let c = match ce with
   | None -> c
@@ -478,42 +478,66 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist.trace in
-  let evdc =
-    catch_error trace 
-      (understand_ltac ~resolve_classes:use_classes expand_evar sigma env vars kind) c 
-  in
   let (evd,c) =
-    if expand_evar then
-      solve_remaining_evars fail_evar use_classes
-        solve_by_implicit_tactic env sigma evdc
-    else
-      evdc in
+    catch_error trace (understand_ltac flags sigma env vars kind) c
+  in
   db_constr ist.debug env c;
   (evd,c)
 
+let constr_flags = {
+  use_typeclasses = true;
+  use_unif_heuristics = true;
+  use_hook = Some solve_by_implicit_tactic;
+  fail_evar = true;
+  expand_evars = true }
+
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  interp_gen kind ist false true true true env sigma c
+  interp_gen kind ist false constr_flags env sigma c
 
-let interp_constr = interp_constr_gen (OfType None)
+let interp_constr = interp_constr_gen WithoutTypeConstraint
 
 let interp_type = interp_constr_gen IsType
 
+let open_constr_use_classes_flags = {
+  use_typeclasses = true;
+  use_unif_heuristics = true;
+  use_hook = Some solve_by_implicit_tactic;
+  fail_evar = false;
+  expand_evars = true }
+
+let open_constr_no_classes_flags = {
+  use_typeclasses = false;
+  use_unif_heuristics = true;
+  use_hook = Some solve_by_implicit_tactic;
+  fail_evar = false;
+  expand_evars = true }
+
+let pure_open_constr_flags = {
+  use_typeclasses = false;
+  use_unif_heuristics = true;
+  use_hook = None;
+  fail_evar = false;
+  expand_evars = false }
+
 (* Interprets an open constr *)
-let interp_open_constr ccl ist =
-  interp_gen (OfType ccl) ist false true false (not (Option.is_empty ccl))
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+  let flags =
+    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
+    else open_constr_use_classes_flags in
+  interp_gen expected_type ist false flags
 
 let interp_pure_open_constr ist =
-  interp_gen (OfType None) ist false false false false
+  interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
 
 let interp_typed_pattern ist env sigma (c,_) =
   let sigma, c =
-    interp_gen (OfType None) ist true false false false env sigma c in
+    interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
   pattern_of_constr sigma c
 
 (* Interprets a constr expression casted by the current goal *)
 let pf_interp_casted_constr ist gl c =
-  interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c
+  interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
 
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
@@ -542,8 +566,7 @@ let interp_constr_list ist env sigma c =
   interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_constr ist env sigma c
 
 let interp_open_constr_list =
-  interp_constr_in_compound_list (fun x -> x) (fun x -> x)
-    (interp_open_constr None)
+  interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr
 
 let interp_auto_lemmas ist env sigma lems =
   let local_sigma, lems = interp_open_constr_list ist env sigma lems in
@@ -743,7 +766,7 @@ let interp_declared_or_quantified_hypothesis ist gl = function
       with Not_found -> NamedHyp id
 
 let interp_binding ist env sigma (loc,b,c) =
-  let sigma, c = interp_open_constr None ist env sigma c in
+  let sigma, c = interp_open_constr ist env sigma c in
   sigma, (loc,interp_binding_name ist b,c)
 
 let interp_bindings ist env sigma = function
@@ -758,12 +781,12 @@ let interp_bindings ist env sigma = function
 
 let interp_constr_with_bindings ist env sigma (c,bl) =
   let sigma, bl = interp_bindings ist env sigma bl in
-  let sigma, c = interp_open_constr None ist env sigma c in
+  let sigma, c = interp_open_constr ist env sigma c in
   sigma, (c,bl)
 
 let interp_open_constr_with_bindings ist env sigma (c,bl) =
   let sigma, bl = interp_bindings ist env sigma bl in
-  let sigma, c = interp_open_constr None ist env sigma c in
+  let sigma, c = interp_open_constr ist env sigma c in
   sigma, (c, bl)
 
 let loc_of_bindings = function
@@ -985,7 +1008,7 @@ let mk_constr_value ist gl c =
   let (sigma,c_interp) = pf_interp_constr ist gl c in
   sigma,VConstr ([],c_interp)
 let mk_open_constr_value ist gl c = 
-  let (sigma,c_interp) = pf_apply (interp_open_constr None ist) gl c in
+  let (sigma,c_interp) = pf_apply (interp_open_constr ist) gl c in
   sigma,VConstr ([],c_interp)
 let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c))
 let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
@@ -1370,8 +1393,10 @@ and interp_genarg ist gl x =
       evdref := sigma;
       in_gen wit_red_expr r_interp
     | OpenConstrArgType casted ->
+      let expected_type =
+        if casted then OfType (pf_concl gl) else WithoutTypeConstraint in
       in_gen (wit_open_constr_gen casted)
-        (interp_open_constr (if casted then Some (pf_concl gl) else None)
+        (interp_open_constr ~expected_type
            ist (pf_env gl) (project gl)
            (snd (out_gen (globwit_open_constr_gen casted) x)))
     | ConstrWithBindingsArgType ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 21487a36dc..0599c52d10 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -79,9 +79,17 @@ let _ =
       optread  = (fun () -> !dependent_propositions_elimination) ;
       optwrite = (fun b -> dependent_propositions_elimination := b) }
 
-let finish_evar_resolution env initial_sigma c =
-  snd (Pretyping.solve_remaining_evars true true solve_by_implicit_tactic
-         env initial_sigma c)
+let tactic_infer_flags = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some solve_by_implicit_tactic;
+  Pretyping.fail_evar = true;
+  Pretyping.expand_evars = true }
+
+let finish_evar_resolution env initial_sigma (sigma,c) =
+  let sigma =
+    Pretyping.solve_remaining_evars tactic_infer_flags env initial_sigma sigma
+  in nf_evar sigma c
 
 (*********************************************)
 (*                 Tactics                   *)
@@ -1110,7 +1118,6 @@ let vm_cast_no_check c gl =
 
 
 let exact_proof c gl =
-  (* on experimente la synthese d'ise dans exact *)
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
   in refine_no_check c gl
 
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 257c55fd80..e42663505d 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -2,21 +2,21 @@
 (* Pattern-matching when non inductive terms occur                          *)
 
 (* Dependent form of annotation *)
-Type match 0 as n, eq return nat with
+Type match 0 as n, @eq return nat with
      | O, x => 0
      | S x, y => x
      end.
-Type match 0, eq, 0 return nat with
+Type match 0, 0, @eq return nat with
      | O, x, y => 0
      | S x, y, z => x
      end.
-Type match 0, eq, 0 return _ with
+Type match 0, @eq, 0 return _ with
      | O, x, y => 0
      | S x, y, z => x
      end.
 
 (* Non dependent form of annotation *)
-Type match 0, eq return nat with
+Type match 0, @eq return nat with
      | O, x => 0
      | S x, y => x
      end.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 7278cc4c1b..9fc5d02787 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -136,7 +136,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
     let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in
+    let c', imps' = interp_type_evars_impls ~impls evars env' tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 85c67a5c7a..aba8a5a81c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -71,7 +71,7 @@ let red_constant_entry n ce = function
       { ce with const_entry_body =
         under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
 
-let interp_definition bl red_option fail_evar c ctypopt =
+let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
@@ -79,7 +79,7 @@ let interp_definition bl red_option fail_evar c ctypopt =
   let imps,ce =
     match ctypopt with
       None ->
-	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar env_bl c in
+	let c, imps2 = interp_constr_evars_impls ~impls evdref env_bl c in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
@@ -89,8 +89,8 @@ let interp_definition bl red_option fail_evar c ctypopt =
 	  const_entry_inline_code = false
 	}
     | Some ctyp ->
-	let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in
-	let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar env_bl c ty in
+	let ty, impsty = interp_type_evars_impls ~impls evdref env_bl ctyp in
+	let c, imps2 = interp_casted_constr_evars_impls ~impls evdref env_bl c ty in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
         let beq b1 b2 = if b1 then b2 else not b2 in
@@ -110,10 +110,8 @@ let interp_definition bl red_option fail_evar c ctypopt =
   red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
 
 let check_definition (ce, evd, imps) =
-  let env = Global.env () in
-    check_evars env Evd.empty evd ce.const_entry_body;
-    Option.iter (check_evars env Evd.empty evd) ce.const_entry_type;
-    ce
+  check_evars_are_solved (Global.env ()) Evd.empty evd;
+  ce
 
 let get_locality id = function
 | Discharge ->
@@ -157,7 +155,7 @@ let declare_definition ident (local, k) ce imps hook =
 let _ = Obligations.declare_definition_ref := declare_definition
 
 let do_definition ident k bl red_option c ctypopt hook =
-  let (ce, evd, imps as def) = interp_definition bl red_option (not (Flags.is_program_mode ())) c ctypopt in
+  let (ce, evd, imps as def) = interp_definition bl red_option c ctypopt in
     if Flags.is_program_mode () then
       let env = Global.env () in
       let c = ce.const_entry_body in
@@ -211,7 +209,7 @@ let set_declare_assumptions_hook = (:=) declare_assumptions_hook
 
 let interp_assumption evdref env bl c =
   let c = prod_constr_expr c bl in
-  interp_type_evars_impls ~evdref ~fail_evar:false env c
+  interp_type_evars_impls evdref env c
 
 let declare_assumptions idl is_coe k c imps impl_is_on nl =
   !declare_assumptions_hook c;
@@ -229,10 +227,8 @@ let do_assumptions kind nl l =
     let env =
       push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
     (env,((is_coe,idl),t,imps))) env l in
-  let evd = consider_remaining_unif_problems env !evdref in
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
+  let evd = solve_remaining_evars all_and_fail_flags env Evd.empty !evdref in
   let l = List.map (on_pi2 (nf_evar evd)) l in
-  List.iter (fun (_,c,_) -> check_evars env Evd.empty evd c) l;
   snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,imps) ->
     let t = replace_vars subst t in
     let (refs,status') = declare_assumptions idl is_coe kind t imps false nl in
@@ -289,14 +285,14 @@ let prepare_param = function
   | (na,Some b,_) -> out_name na, LocalDef b
 
 let interp_ind_arity evdref env ind =
-  interp_type_evars_impls ~evdref ~fail_evar:false env ind.ind_arity
+  interp_type_evars_impls evdref env ind.ind_arity
 
 let interp_cstrs evdref env impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
   (* Complete conclusions of constructor types if given in ML-style syntax *)
   let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
   (* Interpret the constructor types *)
-  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref ~fail_evar:false env ~impls) ctyps') in
+  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in
     (cnames, ctyps'', cimpls)
 
 let interp_mutual_inductive (paramsl,indl) notations finite =
@@ -332,18 +328,11 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
      List.map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl)
      () in
 
-  (* Instantiate evars and check all are resolved *)
-  let evd = consider_remaining_unif_problems env_params !evdref in
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in
-  let sigma = evd in
+  (* Try further to solve evars, and instantiate them *)
+  let sigma = solve_remaining_evars all_and_fail_flags env_params Evd.empty !evdref in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Context.map_rel_context (nf_evar sigma) ctx_params in
   let arities = List.map (nf_evar sigma) arities in
-  List.iter (check_evars env_params Evd.empty evd) arities;
-  Context.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
-  List.iter (fun (_,ctyps,_) ->
-    List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
-    constructors;
 
   (* Build the inductive entries *)
   let entries = List.map3 (fun ind arity (cnames,ctypes,cimpls) -> {
@@ -524,7 +513,7 @@ let interp_fix_context evdref env isfix fix =
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl evdref impls (env,_) fix =
-  interp_type_evars_impls ~impls ~evdref ~fail_evar:false env fix.fix_type
+  interp_type_evars_impls ~impls evdref env fix.fix_type
 
 let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
   Option.map (fun body ->
@@ -634,7 +623,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let arg = (Name argname, None, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
-  let rel, _ = interp_constr_evars_impls ~evdref env r in
+  let rel, _ = interp_constr_evars_impls evdref env r in
+  let () = check_evars_are_solved env Evd.empty !evdref in
   let relty = Typing.type_of env !evdref rel in
   let relargty =
     let error () =
@@ -807,18 +797,22 @@ let interp_recursive isfix fixl notations =
   (* Build the fix declaration block *)
   (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
 
-let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
-  List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs;
-  List.iter (check_evars env Evd.empty evd) fixtypes;
+let check_recursive isfix env evd (fixnames,fixdefs,_) =
+  check_evars_are_solved env Evd.empty evd;
   if not (List.mem None fixdefs) then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env isfix (List.combine fixnames fixdefs)
-  end;
-  ((fixnames,fixdefs,fixtypes),info)
+  end
+
+let interp_fixpoint l ntns =
+  let (env,_,evd),fix,info = interp_recursive true l ntns in
+  check_recursive true env evd fix;
+  fix,info
 
-let interp_fixpoint l ntns = check_recursive true (interp_recursive true l ntns)
-let interp_cofixpoint l ntns = check_recursive false (interp_recursive false l ntns)
+let interp_cofixpoint l ntns =
+  let (env,_,evd),fix,info = interp_recursive false l ntns in
+  check_recursive false  env evd fix;
+  fix,info
     
 let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 6d4f6c09c4..f38d954a17 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -32,7 +32,7 @@ val set_declare_assumptions_hook : (types -> unit) -> unit
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  local_binder list -> red_expr option -> bool (* Fail if evars remain *) -> constr_expr ->
+  local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index b237a47622..1d953806dc 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -343,8 +343,8 @@ let start_proof_com kind thms hook =
   let env0 = Global.env () in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in
-    let t', imps' = interp_type_evars_impls ~impls ~evdref env t in
-    Context.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
+    let t', imps' = interp_type_evars_impls ~impls evdref env t in
+    check_evars_are_solved env Evd.empty !evdref;
     let ids = List.map pi1 ctx in
       (compute_proof_name (fst kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c5ec2d7e9e..ff918293b5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -26,16 +26,11 @@ open Constrexpr_ops
 
 (********** definition d'un record (structure) **************)
 
-let interp_evars evdref env impls k typ =
-  let typ' = intern_gen Pretyping.IsType ~impls !evdref env typ in
-  let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
-    imps, Pretyping.understand_tcc_evars evdref env k typ'
-
 let interp_fields_evars evars env impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
-      let impl, t' = interp_evars evars env impls Pretyping.IsType t in
-      let b' = Option.map (fun x -> snd (interp_evars evars env impls (Pretyping.OfType (Some t')) x)) b in
+      let t', impl = interp_type_evars_impls evars env ~impls t in
+      let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls evars env ~impls x t')) b in
       let impls =
 	match i with
 	| Anonymous -> impls
@@ -72,14 +67,9 @@ let typecheck_params_and_fields id t ps nots fs =
   let env2,impls,newfs,data =
     interp_fields_evars evars env_ar impls_env nots (binders_of_decls fs)
   in
-  let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
-  let evars = Typeclasses.resolve_typeclasses env_ar evars in
-  let sigma =  evars in
+  let sigma = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in
   let newps = Evarutil.nf_rel_context_evar sigma newps in
   let newfs = Evarutil.nf_rel_context_evar sigma newfs in
-  let ce t = Evarutil.check_evars env0 Evd.empty evars t in
-    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
-    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
     imps, newps, impls, newfs
 
 let degenerate_decl (na,b,t) =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3395bea150..b1a1cf03c6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1379,7 +1379,7 @@ let vernac_check_may_eval redexp glopt rc =
   let module P = Pretype_errors in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr sigma env rc in
-  let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
+  Evarconv.check_problems_are_solved sigma';
   let j =
     try
       Evarutil.check_evars env sigma sigma' c;