From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 29 Apr 2010 09:56:37 +0000 Subject: Move from ocamlweb to ocamdoc to generate mli documentation dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/environ.mli | 126 ++++++++++++++++++++++++++--------------------------- 1 file changed, 63 insertions(+), 63 deletions(-) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli index 667a0ed43..fce149e10 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,26 +1,24 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* named_context_val val engagement : env -> engagement option -(* is the local context empty *) +(** is the local context empty *) val empty_context : env -> bool -(************************************************************************) -(*s Context of de Bruijn variables ([rel_context]) *) +(** {5 Context of de Bruijn variables ([rel_context]) } *) + val nb_rel : env -> int val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env -(* Looks up in the context of local vars referred by indice ([rel_context]) *) -(* raises [Not_found] if the index points out of the context *) +(** Looks up in the context of local vars referred by indice ([rel_context]) + raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> rel_declaration val evaluable_rel : int -> env -> bool -(*s Recurrence on [rel_context] *) +(** {6 Recurrence on [rel_context] } *) + val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a -(************************************************************************) -(* Context of variables (section variables and goal assumptions) *) +(** {5 Context of variables (section variables and goal assumptions) } *) val named_context_of_val : named_context_val -> named_context val named_vals_of_val : named_context_val -> Pre_env.named_vals @@ -78,7 +76,7 @@ val val_of_named_context : named_context -> named_context_val val empty_named_context_val : named_context_val -(* [map_named_val f ctxt] apply [f] to the body and the type of +(** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) val map_named_val : @@ -90,8 +88,8 @@ val push_named_context_val : -(* Looks up in the context of local vars referred by names ([named_context]) *) -(* raises [Not_found] if the identifier is not found *) +(** Looks up in the context of local vars referred by names ([named_context]) + raises [Not_found] if the identifier is not found *) val lookup_named : variable -> env -> named_declaration val lookup_named_val : variable -> named_context_val -> named_declaration @@ -99,34 +97,36 @@ val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option -(*s Recurrence on [named_context]: older declarations processed first *) +(** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a -(* Recurrence on [named_context] starting from younger decl *) +(** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a -(* This forgets named and rel contexts *) +(** This forgets named and rel contexts *) val reset_context : env -> env -(* This forgets rel context and sets a new named context *) + +(** This forgets rel context and sets a new named context *) val reset_with_named_context : named_context_val -> env -> env -(************************************************************************) -(*s Global constants *) -(*s Add entries to global environment *) -val add_constant : constant -> constant_body -> env -> env +(** {5 Global constants } + {6 Add entries to global environment } *) -(* Looks up in the context of global constant names *) -(* raises [Not_found] if the required path is not found *) +val add_constant : constant -> constant_body -> env -> env +(** Looks up in the context of global constant names + raises [Not_found] if the required path is not found *) val lookup_constant : constant -> env -> constant_body val evaluable_constant : constant -> env -> bool -(*s [constant_value env c] raises [NotEvaluableConst Opaque] if +(** {6 Sect } *) +(** [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no body and [Not_found] if it does not exist in [env] *) + type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result @@ -134,44 +134,45 @@ val constant_value : env -> constant -> constr val constant_type : env -> constant -> constant_type val constant_opt_value : env -> constant -> constr option -(************************************************************************) -(*s Inductive types *) +(** {5 Inductive types } *) + val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env -(* Looks up in the context of global inductive names *) -(* raises [Not_found] if the required path is not found *) +(** Looks up in the context of global inductive names + raises [Not_found] if the required path is not found *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body -(************************************************************************) -(*s Modules *) +(** {5 Modules } *) + val add_modtype : module_path -> module_type_body -> env -> env -(* [shallow_add_module] does not add module components *) +(** [shallow_add_module] does not add module components *) val shallow_add_module : module_path -> module_body -> env -> env val lookup_module : module_path -> env -> module_body val lookup_modtype : module_path -> env -> module_type_body -(************************************************************************) -(*s Universe constraints *) +(** {5 Universe constraints } *) + val set_universes : Univ.universes -> env -> env val add_constraints : Univ.constraints -> env -> env val set_engagement : engagement -> env -> env -(************************************************************************) -(* Sets of referred section variables *) -(* [global_vars_set env c] returns the list of [id]'s occurring either +(** {6 Sets of referred section variables } + [global_vars_set env c] returns the list of [id]'s occurring either directly as [Var id] in [c] or indirectly as a section variable dependent in a global reference occurring in [c] *) + val global_vars_set : env -> constr -> Idset.t -(* the constr must be a global reference *) + +(** the constr must be a global reference *) val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context -(************************************************************************) -(*s Unsafe judgments. We introduce here the pre-type of judgments, which is +(** {5 Unsafe judgments. } + We introduce here the pre-type of judgments, which is actually only a datatype to store a term with its type and the type of its type. *) @@ -188,23 +189,22 @@ type unsafe_type_judgment = { utj_type : sorts } -(*s Compilation of global declaration *) +(** {6 Compilation of global declaration } *) val compile_constant_body : env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code - (* opaque *) (* boxed *) + (** opaque *) (* boxed *) exception Hyp_not_found -(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and +(** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and return [tail::(f head (id,_,_) (rev tail))::head]. the value associated to id should not change *) - val apply_to_hyp : named_context_val -> variable -> (named_context -> named_declaration -> named_context -> named_declaration) -> named_context_val -(* [apply_to_hyp_and_dependent_on sign id f g] split [sign] into +(** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into [tail::(id,_,_)::head] and return [(g tail)::(f (id,_,_))::head]. *) val apply_to_hyp_and_dependent_on : named_context_val -> variable -> @@ -219,9 +219,10 @@ val insert_after_hyp : named_context_val -> variable -> val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val -(* spiwack: functions manipulating the retroknowledge *) -open Retroknowledge +open Retroknowledge +(** functions manipulating the retroknowledge + @author spiwack *) val retroknowledge : (retroknowledge->'a) -> env -> 'a val registered : env -> field -> bool @@ -232,19 +233,18 @@ val register : env -> field -> Retroknowledge.entry -> env -(******************************************************************) -(* spiwack: a few declarations for the "Print Assumption" command *) - +(** a few declarations for the "Print Assumption" command + @author spiwack *) type context_object = - | Variable of identifier (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) - | Opaque of constant (* An opaque constant. *) + | Variable of identifier (** A section variable or a Let definition *) + | Axiom of constant (** An axiom or a constant. *) + | Opaque of constant (** An opaque constant. *) -(* AssumptionSet.t is a set of [assumption] *) +(** AssumptionSet.t is a set of [assumption] *) module OrderedContextObject : Set.OrderedType with type t = context_object module ContextObjectMap : Map.S with type key = context_object -(* collects all the assumptions (optionally including opaque definitions) +(** collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type) *) val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t -- cgit v1.2.3