diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /library/lib.mli | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'library/lib.mli')
-rw-r--r-- | library/lib.mli | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/library/lib.mli b/library/lib.mli index 64074cfd..d35fcc09 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 11046 2008-06-03 22:48:06Z msozeau $ i*) +(*i $Id: lib.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Util @@ -171,17 +171,24 @@ val reset_initial : unit -> unit val set_xml_open_section : (identifier -> unit) -> unit val set_xml_close_section : (identifier -> unit) -> unit +type binding_kind = Explicit | Implicit (*s Section management for discharge *) +type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types +type variable_context = variable_info list -val section_segment_of_constant : constant -> Sign.named_context -val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context +val instance_from_variable_context : variable_context -> Names.identifier array +val named_of_variable_context : variable_context -> Sign.named_context -val section_instance : global_reference -> identifier array +val section_segment_of_constant : Names.constant -> variable_context +val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context -val add_section_variable : identifier -> bool -> Term.types option -> unit -val add_section_constant : constant -> Sign.named_context -> unit -val add_section_kn : kernel_name -> Sign.named_context -> unit +val section_instance : Libnames.global_reference -> Names.identifier array +val is_in_section : Libnames.global_reference -> bool + +val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit +val add_section_constant : Names.constant -> Sign.named_context -> unit +val add_section_kn : Names.kernel_name -> Sign.named_context -> unit val replacement_context : unit -> (identifier array Cmap.t * identifier array KNmap.t) |