diff options
author | 2013-05-09 18:05:50 +0000 | |
---|---|---|
committer | 2013-05-09 18:05:50 +0000 | |
commit | 78a5b30be750c517d529f9f2b8a291699d5d92e6 (patch) | |
tree | 7e3c19f0b9a4bc71ed6e780e48bc427833a84872 /proofs/goal.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 'proofs/goal.ml')
-rw-r--r-- | proofs/goal.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 6b794c147..67cd41412 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -111,9 +111,7 @@ let return v _ _ _ _ = v In an ideal world, this could/should be the other way round. As of now, though, it seems at least quite useful to build tactics. *) let interp_constr cexpr env rdefs _ _ = - let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in - rdefs := defs ; - c + Constrintern.interp_constr_evars rdefs env cexpr (* Type of constr with holes used by refine. *) (* The list of evars doesn't necessarily contain all the evars in the constr, @@ -217,11 +215,14 @@ module Refinable = struct let init_defs = !rdefs in (* if [check_type] is true, then creates a type constraint for the proof-to-be *) - let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in + let tycon = if check_type then Pretyping.OfType (Evd.evar_concl info) else Pretyping.WithoutTypeConstraint in (* call to [understand_tcc_evars] returns a constr with undefined evars these evars will be our new goals *) + let flags = + if resolve_classes then Pretyping.all_no_fail_flags + else Pretyping.no_classes_no_fail_inference_flags in let open_constr = - Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc + Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc in ignore(update_handle handle init_defs !rdefs); open_constr |