From fc3f8eb9bcb6645a97a35335d588dbd50231689b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 8 Apr 2008 16:15:23 +0000
Subject: - A little cleanup in Classes/*. Separate standard morphisms on
 relf/sym/trans relations from morphisms on prop connectives and relations. -
 Add general order theory on predicates, instantiated for relations. Derives
 equivalence, implication, conjunction and disjunction as liftings from
 propositional connectives. Can be used for n-ary homogeneous predicates
 thanks to a bit of metaprogramming with lists of types. - Rebind
 Setoid_Theory to use the Equivalence record type instead of declaring an
 isomorphic one. One needs to do "red" after constructor to get the same
 statements when building objects of type Setoid_Theory, so scripts break.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/classes.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index bc627a2836..203fe118d3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -552,8 +552,9 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	      Flags.silently (fun () ->
 		Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
-		Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
-		  (!refine_ref (evm, term));
+		if props <> [] then 
+		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+		    (!refine_ref (evm, term));
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
 	      id
-- 
cgit v1.2.3