diff options
| author | msozeau | 2008-02-10 14:10:38 +0000 |
|---|---|---|
| committer | msozeau | 2008-02-10 14:10:38 +0000 |
| commit | ee90aac584d123fa709d6629d99057b62bb343d0 (patch) | |
| tree | 242267d42f56a952af775f1eb04d94378d171836 /tactics/class_setoid.ml4 | |
| parent | 952d9ebd44fe6bd052c81c583e3a74752b53f932 (diff) | |
Backport Program Instance into Instance. Proper early error message if
trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_setoid.ml4')
| -rw-r--r-- | tactics/class_setoid.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index 9aa4451870..5939f840fc 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -397,3 +397,6 @@ TACTIC EXTEND typeclasses_eauto let evd' = resolve_argument_typeclasses d (mode, depth) env evd false false in Refiner.tclEVARS (Evd.evars_of evd') gl ] END + +let _ = + Classes.refine_ref := Refine.refine |