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

1 files changed, 19 insertions, 0 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 =