diff options
Diffstat (limited to 'interp/constrextern.mli')
-rw-r--r-- | interp/constrextern.mli | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 08a74e614..f52ec8fd8 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.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 Util open Names open Term @@ -21,12 +20,11 @@ open Rawterm open Pattern open Topconstr open Notation -(*i*) -(* v7->v8 translation *) +(** v7->v8 translation *) val check_same_type : constr_expr -> constr_expr -> unit -(* Translation of pattern, cases pattern, rawterm and term into syntax +(** Translation of pattern, cases pattern, rawterm and term into syntax trees for printing *) val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr @@ -34,7 +32,7 @@ val extern_rawconstr : Idset.t -> rawconstr -> constr_expr val extern_rawtype : Idset.t -> rawconstr -> constr_expr val extern_constr_pattern : names_context -> constr_pattern -> constr_expr -(* If [b=true] in [extern_constr b env c] then the variables in the first +(** If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed *) val extern_constr : bool -> env -> constr -> constr_expr @@ -45,7 +43,7 @@ val extern_sort : sorts -> rawsort val extern_rel_context : constr option -> env -> rel_context -> local_binder list -(* Printing options *) +(** Printing options *) val print_implicits : bool ref val print_implicits_defensive : bool ref val print_arguments : bool ref @@ -55,25 +53,25 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -(* Debug printing options *) +(** Debug printing options *) val set_debug_global_reference_printer : (loc -> global_reference -> reference) -> unit -(* This governs printing of implicit arguments. If [with_implicits] is +(** This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed by "!"; if [with_implicits] and [with_arguments] are both on the function and not the arguments is prefixed by "!" *) val with_implicits : ('a -> 'b) -> 'a -> 'b val with_arguments : ('a -> 'b) -> 'a -> 'b -(* This forces printing of coercions *) +(** This forces printing of coercions *) val with_coercions : ('a -> 'b) -> 'a -> 'b -(* This forces printing universe names of Type{.} *) +(** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b -(* This suppresses printing of numeral and symbols *) +(** This suppresses printing of numeral and symbols *) val without_symbols : ('a -> 'b) -> 'a -> 'b -(* This prints metas as anonymous holes *) +(** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b |