diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-09 18:05:50 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-09 18:05:50 +0000 |
commit | 78a5b30be750c517d529f9f2b8a291699d5d92e6 (patch) | |
tree | 7e3c19f0b9a4bc71ed6e780e48bc427833a84872 /proofs/pfedit.mli | |
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 'proofs/pfedit.mli')
-rw-r--r-- | proofs/pfedit.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 4ca23e711..73850c6f0 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 |