diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 14:10:38 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 14:10:38 +0000 |
| commit | ee90aac584d123fa709d6629d99057b62bb343d0 (patch) | |
| tree | 242267d42f56a952af775f1eb04d94378d171836 /toplevel/command.mli | |
| 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 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index d587fabf7..7ec29e0f5 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -30,6 +30,8 @@ open Redexpr functions of [Declare]; they return an absolute reference to the defined object *) +val definition_message : identifier -> unit + val declare_definition : identifier -> definition_kind -> local_binder list -> red_expr option -> constr_expr -> constr_expr option -> declaration_hook -> unit |