From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 pretyping/pretype_errors.mli | 74 ++++++++++++++++++++++----------------------
 1 file changed, 37 insertions(+), 37 deletions(-)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d3e6ffea..3a3dccb4 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -1,30 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretype_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Pp
 open Util
 open Names
 open Term
 open Sign
 open Environ
-open Rawterm
+open Glob_term
 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 *
@@ -37,51 +33,55 @@ type pretype_error =
   | CannotFindWellTypedAbstraction of constr * constr list
   | AbstractionOverMeta of name * name
   | NonLinearUnification of name * constr
-  (* Pretyping *)
+  (** Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of Type_errors.type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 val precatchable_exception : exn -> bool
 
-(* 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 :
-   Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
-   Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
-   Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+(** 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 : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+
+val env_nf_evar : Evd.evar_map -> env -> env
+val env_nf_betaiotaevar : Evd.evar_map -> env -> env
 
+val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jv_nf_betaiotaevar :
+  Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 
-(* Raising errors *)
+(** Raising errors *)
 val error_actual_type_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc :
-  loc -> env ->  Evd.evar_map -> int * constr * constr ->
+  loc -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc :
-  loc -> env ->  Evd.evar_map ->
-      constr -> int -> constr -> constr -> 'b
+  loc -> env -> Evd.evar_map ->
+      constr -> constructor -> constr -> constr -> 'b
 
 val error_number_branches_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
@@ -89,9 +89,9 @@ 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
+val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
   env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
@@ -113,19 +113,19 @@ val error_abstraction_over_meta : env -> Evd.evar_map ->
 val error_non_linear_unification : env -> Evd.evar_map ->
   metavariable -> constr -> 'b
 
-(*s Ml Case errors *)
+(** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  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
+  loc -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
-(*s Error in conversion from AST to rawterms *)
+(** {6 Error in conversion from AST to glob_constr } *)
 
 val error_var_not_found_loc : loc -> identifier -> 'b
-- 
cgit v1.2.3