diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:34:26 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:34:26 +0000 |
| commit | 0a1202fae3a8ae8cf651c1b699545a8638ec579f (patch) | |
| tree | 652b6ae0fa3458d114467c31e1fe382bd1b755a3 /tactics/class_tactics.ml | |
| parent | fe9258c4b228fb086baac7cd3d94207f2c43bb48 (diff) | |
A whole new implemenation of the refine tactic.
It now uses the same algorithm as pretyping does.
This produces pretty weird goal when refining pattern matching terms.
Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now.
The file Zsqrt_compat.v has two temporary [Admitted] related to this issue.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c1c1c5f14..1aaf4af00 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -725,7 +725,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl let _ = Classes.refine_ref := begin fun c -> - Refine.refine c + Tactics.New.refine c end (** Take the head of the arity of a constr. |