diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 09:56:37 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 09:56:37 +0000 |
commit | f73d7c4614d000f068550b5144d80b7eceed58e9 (patch) | |
tree | 4fa9a679a6e55269cc5c7cf24fce725acb2574b5 /interp/constrintern.mli | |
parent | 552e596e81362e348fc17fcebcc428005934bed6 (diff) |
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
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r-- | interp/constrintern.mli | 55 |
1 files changed, 27 insertions, 28 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 5a62541db..4ba2bc587 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Term open Sign @@ -20,9 +19,9 @@ open Pattern open Topconstr open Termops open Pretyping -(*i*) -(*s Translation from front abstract syntax of term to untyped terms (rawconstr) +(** {6 Sect } *) +(** Translation from front abstract syntax of term to untyped terms (rawconstr) The translation performs: @@ -33,7 +32,7 @@ open Pretyping - insert existential variables for implicit arguments *) -(* To interpret implicits and arg scopes of recursive variables while +(** To interpret implicits and arg scopes of recursive variables while internalizing inductive types and recursive definitions, and also projection while typing records. @@ -49,11 +48,11 @@ type var_internalization_data = Impargs.implicits_list * scope_name option list -(* A map of free variables to their implicit arguments and scopes *) +(** A map of free variables to their implicit arguments and scopes *) type internalization_env = (identifier * var_internalization_data) list -(* Contains also a list of identifiers to automatically apply to the variables*) +(** Contains also a list of identifiers to automatically apply to the variables*) type full_internalization_env = identifier list * internalization_env @@ -76,7 +75,7 @@ type ltac_sign = identifier list * unbound_ltac_var_map type raw_binder = (name * binding_kind * rawconstr option * rawconstr) -(*s Internalisation performs interpretation of global names and notations *) +(** {6 Internalisation performs interpretation of global names and notations } *) val intern_constr : evar_map -> env -> constr_expr -> rawconstr @@ -92,15 +91,15 @@ val intern_pattern : env -> cases_pattern_expr -> val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list -(*s Composing internalization with pretyping *) +(** {6 Composing internalization with pretyping } *) -(* Main interpretation function *) +(** Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr -(* Particular instances *) +(** Particular instances *) val interp_constr : evar_map -> env -> constr_expr -> constr @@ -115,7 +114,7 @@ val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * c val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr -(* Accepting evars and giving back the manual implicits in addition. *) +(** Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits @@ -134,29 +133,29 @@ val interp_casted_constr_evars : evar_map ref -> env -> val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types -(*s Build a judgment *) +(** {6 Build a judgment } *) val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment -(* Interprets constr patterns *) +(** Interprets constr patterns *) val intern_constr_pattern : evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern -(* Raise Not_found if syndef not bound to a name and error if unexisting ref *) +(** Raise Not_found if syndef not bound to a name and error if unexisting ref *) val intern_reference : reference -> global_reference -(* Expands abbreviations (syndef); raise an error if not existing *) +(** Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> reference -> rawconstr -(* Interpret binders *) +(** Interpret binders *) val interp_binder : evar_map -> env -> name -> constr_expr -> types val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types -(* Interpret contexts: returns extended env and context *) +(** Interpret contexts: returns extended env and context *) val interp_context_gen : (env -> rawconstr -> types) -> (env -> rawconstr -> unsafe_judgment) -> @@ -169,18 +168,18 @@ val interp_context : ?fail_anonymous:bool -> val interp_context_evars : ?fail_anonymous:bool -> evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits -(* Locating references of constructions, possibly via a syntactic definition *) -(* (these functions do not modify the glob file) *) +(** Locating references of constructions, possibly via a syntactic definition + (these functions do not modify the glob file) *) val is_global : identifier -> bool val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr -(* Interprets into a abbreviatable constr *) +(** Interprets into a abbreviatable constr *) val interp_aconstr : ?impls:full_internalization_env -> identifier list * identifier list -> constr_expr -> interpretation -(* Globalization leak for Grammar *) +(** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b |