From ee90aac584d123fa709d6629d99057b62bb343d0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 10 Feb 2008 14:10:38 +0000
Subject: 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
---
 tactics/class_setoid.ml4 | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tactics')

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
-- 
cgit v1.2.3