diff options
author | 2013-05-09 18:05:50 +0000 | |
---|---|---|
committer | 2013-05-09 18:05:50 +0000 | |
commit | 78a5b30be750c517d529f9f2b8a291699d5d92e6 (patch) | |
tree | 7e3c19f0b9a4bc71ed6e780e48bc427833a84872 /test-suite | |
parent | 38f734040d5fad0f5170a1fdee6f96e3e4f1c06d (diff) |
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
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/Cases.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 257c55fd8..e42663505 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. |