diff options
| author | msozeau | 2008-04-08 16:15:23 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-08 16:15:23 +0000 |
| commit | fc3f8eb9bcb6645a97a35335d588dbd50231689b (patch) | |
| tree | ffc084a3a1d5a08fd5704a321abef2d58ff1e519 /toplevel | |
| parent | 98f930742ca58742a9bc0a575e2d362ee2fa061e (diff) | |
- 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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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 |