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

4 files changed, 16 insertions, 9 deletions

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