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

3 files changed, 61 insertions, 29 deletions

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