diff options
| author | msozeau | 2009-09-14 16:57:14 +0000 |
|---|---|---|
| committer | msozeau | 2009-09-14 16:57:14 +0000 |
| commit | a3645985be17e9fa8a8a5c4221aea40e189682c2 (patch) | |
| tree | 8f7f99638e715861976c69bb4df0b9bdeda120e2 /toplevel/command.mli | |
| parent | a764cfdbdfaecaa02f2fff0234fe1a198e0e34b5 (diff) | |
Backtrack on the forced discharge of type class variables introduced
by Context. Now Context has exactly the same semantics as Variables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index d5283a6db6..d648fc10e0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr -> val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> Impargs.manual_explicitation list -> - bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located -> unit + bool (* implicit *) -> bool (* inline *) -> Names.variable located -> unit val set_declare_assumption_hook : (types -> unit) -> unit val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> - bool -> identifier list -> bool -> unit + bool -> bool -> unit val open_temp_scopes : Topconstr.scope_name option -> unit |