diff options
| author | msozeau | 2008-03-23 22:11:25 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-23 22:11:25 +0000 |
| commit | 95dd7304f68eb155f572bf221c4d99fca85b700c (patch) | |
| tree | 8e78cb9ed1eee1939b327cbc0d013f8a99ea4570 /toplevel/command.mli | |
| parent | 32c11b16f7d7ff0ea3aee584103bd60f5b94dedb (diff) | |
Fix a bug found by B. Grégoire when declaring morphisms in module
types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations), explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index a6a403c035..31420d1891 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -33,6 +33,7 @@ open Redexpr val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit val definition_message : identifier -> unit +val assumption_message : identifier -> unit val declare_definition : identifier -> definition_kind -> local_binder list -> red_expr option -> constr_expr -> |