diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:27:54 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:27:54 +0000 |
| commit | f7c2010c34adbc5c20e14909546c0964a32764cc (patch) | |
| tree | 6355a75c786d9c37be0e05bb9e6008b20e50b6dc /tactics/class_tactics.ml4 | |
| parent | 03b12cc43ce24e708f0edb1b4ac3931d42527343 (diff) | |
- Improve unification (beta-reduction, and same heuristic as evarconv for reducing matches).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index d7ead8b7e..4dfe03500 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -354,7 +354,7 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk (fun {it=gls';sigma=s'} fk' -> let needs_backtrack = if gls' = [] then - dependent info.only_classes s' info.is_evar (Goal.V82.concl s' gl) + dependent info.only_classes s' info.is_evar (Goal.V82.concl s gl) else true in let fk'' = if not needs_backtrack then @@ -586,7 +586,7 @@ let resolve_all_evars debug m env p oevd do_split fail = then (* Unable to satisfy the constraints. *) error_unresolvable env comp do_split evd else (* Best effort: do nothing on this component *) - docomp oevd comps + docomp evd comps in docomp oevd split let initial_select_evars onlyargs = |