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

5 files changed, 6 insertions, 6 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index b9334801c..c4d6a7a30 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 5e55bcfb2..70c7f8d1f 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 e98a0952b..e1de8be82 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 fcd1c5360..2a0bbd7b7 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 34085dca2..4b9704c2c 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