diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
| -rw-r--r-- | pretyping/pretype_errors.mli | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index ca48f70211..9b6216a126 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.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 Pp open Util open Names @@ -17,14 +16,13 @@ open Sign open Environ open Rawterm open Inductiveops -(*i*) -(*s The type of errors raised by the pretyper *) +(** {6 The type of errors raised by the pretyper } *) type pretype_error = - (* Old Case *) + (** Old Case *) | CantFindCaseType of constr - (* Unification *) + (** Unification *) | OccurCheck of existential_key * constr | NotClean of existential_key * constr * Evd.hole_kind | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * @@ -35,7 +33,7 @@ type pretype_error = | CannotGeneralize of constr | NoOccurrenceFound of constr * identifier option | CannotFindWellTypedAbstraction of constr * constr list - (* Pretyping *) + (** Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr | NotProduct of constr @@ -44,7 +42,7 @@ exception PretypeError of env * pretype_error val precatchable_exception : exn -> bool -(* Presenting terms without solved evars *) +(** Presenting terms without solved evars *) val nf_evar : Evd.evar_map -> constr -> constr val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment val jl_nf_evar : @@ -55,7 +53,7 @@ val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment -(* Raising errors *) +(** Raising errors *) val error_actual_type_loc : loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b @@ -87,7 +85,7 @@ val error_not_a_type_loc : val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b -(*s Implicit arguments synthesis errors *) +(** {6 Implicit arguments synthesis errors } *) val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b @@ -105,12 +103,12 @@ val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr - val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> constr -> constr list -> 'b -(*s Ml Case errors *) +(** {6 Ml Case errors } *) val error_cant_find_case_type_loc : loc -> env -> Evd.evar_map -> constr -> 'b -(*s Pretyping errors *) +(** {6 Pretyping errors } *) val error_unexpected_type_loc : loc -> env -> Evd.evar_map -> constr -> constr -> 'b @@ -118,6 +116,6 @@ val error_unexpected_type_loc : val error_not_product_loc : loc -> env -> Evd.evar_map -> constr -> 'b -(*s Error in conversion from AST to rawterms *) +(** {6 Error in conversion from AST to rawterms } *) val error_var_not_found_loc : loc -> identifier -> 'b |