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 /tactics/tactics.ml | |
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 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 21487a36d..0599c52d1 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 |