From 83607f75a13ea915affa8cfc5bfc14cc944c61ef Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 18:45:55 +0100 Subject: Find_subterm API using EConstr. --- pretyping/pretype_errors.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 73f81923ff..b015add799 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -28,7 +28,7 @@ type unification_error = type position = (Id.t * Locus.hyp_location_flag) option -type position_reporting = (position * int) * constr +type position_reporting = (position * int) * EConstr.t type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option -- cgit v1.2.3 From 147afe827dc83602cc160a8b1357e84ecea910ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 20:13:32 +0100 Subject: Evardefine API using EConstr. --- pretyping/pretype_errors.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index b015add799..8a6d8b6b37 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -45,14 +45,14 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr (** Pretyping *) | VarNotFound of Id.t | UnexpectedType of constr * constr - | NotProduct of constr + | NotProduct of EConstr.constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of @@ -110,7 +110,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - constr -> constr list -> (env * type_error) option -> 'b + constr -> EConstr.constr list -> (env * type_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> Name.t -> constr -> types -> types -> 'b @@ -132,7 +132,7 @@ val error_unexpected_type : ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b val error_not_product : - ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b (** {6 Error in conversion from AST to glob_constr } *) -- cgit v1.2.3 From b7fd585b89ac5e0b7770f52739c33fe179f2eed8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 21:36:40 +0100 Subject: Evarsolve API using EConstr. --- pretyping/pretype_errors.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 8a6d8b6b37..217deda4d8 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -14,14 +14,14 @@ open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | OccurCheck of existential_key * EConstr.constr + | NotClean of EConstr.existential * env * EConstr.constr | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * EConstr.constr * EConstr.constr | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities -- cgit v1.2.3 From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Nov 2016 11:39:27 +0100 Subject: Unification API using EConstr. --- pretyping/pretype_errors.mli | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 217deda4d8..2e707a0ffc 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -30,7 +30,7 @@ type position = (Id.t * Locus.hyp_location_flag) option type position_reporting = (position * int) * EConstr.t -type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option +type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option type pretype_error = (** Old Case *) @@ -38,17 +38,17 @@ type pretype_error = (** Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * constr + | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option - | CannotUnify of constr * constr * unification_error option - | CannotUnifyLocal of constr * constr * constr + | CannotUnify of EConstr.constr * EConstr.constr * unification_error option + | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr - | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option - | WrongAbstractionType of Name.t * constr * types * types + | NoOccurrenceFound of EConstr.constr * Id.t option + | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option + | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types | AbstractionOverMeta of Name.t * Name.t - | NonLinearUnification of Name.t * constr + | NonLinearUnification of Name.t * EConstr.constr (** Pretyping *) | VarNotFound of Id.t | UnexpectedType of constr * constr @@ -94,32 +94,32 @@ val error_ill_typed_rec_body : val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b -val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b +val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b (** {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 -> EConstr.constr -> 'b val error_unsolvable_implicit : ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> - ?reason:unification_error -> constr * constr -> 'b + ?reason:unification_error -> EConstr.constr * EConstr.constr -> 'b -val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b +val error_cannot_unify_local : env -> Evd.evar_map -> EConstr.constr * EConstr.constr * EConstr.constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - constr -> EConstr.constr list -> (env * type_error) option -> 'b + EConstr.constr -> EConstr.constr list -> (env * type_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> - Name.t -> constr -> types -> types -> 'b + Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b val error_abstraction_over_meta : env -> Evd.evar_map -> metavariable -> metavariable -> 'b val error_non_linear_unification : env -> Evd.evar_map -> - metavariable -> constr -> 'b + metavariable -> EConstr.constr -> 'b (** {6 Ml Case errors } *) -- cgit v1.2.3 From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- pretyping/pretype_errors.mli | 41 +++++++++++++++++++++++++++-------------- 1 file changed, 27 insertions(+), 14 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 2e707a0ffc..0ebe4817ca 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -32,11 +32,13 @@ type position_reporting = (position * int) * EConstr.t type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type type_error = (EConstr.constr, EConstr.types) ptype_error + type pretype_error = (** Old Case *) - | CantFindCaseType of constr + | CantFindCaseType of EConstr.constr (** Type inference unification *) - | ActualTypeNotCoercible of unsafe_judgment * types * unification_error + | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error (** Tactic Unification *) | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option @@ -51,7 +53,7 @@ type pretype_error = | NonLinearUnification of Name.t * EConstr.constr (** Pretyping *) | VarNotFound of Id.t - | UnexpectedType of constr * constr + | UnexpectedType of EConstr.constr * EConstr.constr | NotProduct of EConstr.constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error @@ -65,34 +67,45 @@ val precatchable_exception : exn -> bool (** Raising errors *) val error_actual_type : - ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> unification_error -> 'b +val error_actual_type_core : + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b + val error_cant_apply_not_functional : ?loc:Loc.t -> env -> Evd.evar_map -> - unsafe_judgment -> unsafe_judgment list -> 'b + EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b val error_cant_apply_bad_type : - ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> - unsafe_judgment -> unsafe_judgment list -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr -> + EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b val error_case_not_inductive : - ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b val error_ill_formed_branch : ?loc:Loc.t -> env -> Evd.evar_map -> - constr -> pconstructor -> constr -> constr -> 'b + EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b val error_number_branches : ?loc:Loc.t -> env -> Evd.evar_map -> - unsafe_judgment -> int -> 'b + EConstr.unsafe_judgment -> int -> 'b val error_ill_typed_rec_body : ?loc:Loc.t -> env -> Evd.evar_map -> - int -> Name.t array -> unsafe_judgment array -> types array -> 'b + int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b + +val error_elim_arity : + ?loc:Loc.t -> env -> Evd.evar_map -> + pinductive -> sorts_family list -> EConstr.constr -> + EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b val error_not_a_type : - ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + +val error_assumption : + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b @@ -124,12 +137,12 @@ val error_non_linear_unification : env -> Evd.evar_map -> (** {6 Ml Case errors } *) val error_cant_find_case_type : - ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type : - ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b val error_not_product : ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b -- cgit v1.2.3 From 8beca748d992cd08e2dd7448c8b28dadbcea4a16 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:09:11 +0100 Subject: Cleaning up interfaces. We make mli files look to what they were looking before the move to EConstr by opening this module. --- pretyping/pretype_errors.mli | 87 ++++++++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 43 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 0ebe4817ca..7cef14339b 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -9,52 +9,53 @@ open Names open Term open Environ +open EConstr open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * EConstr.constr - | NotClean of EConstr.existential * env * EConstr.constr + | OccurCheck of existential_key * constr + | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * EConstr.constr * EConstr.constr + | ConversionFailed of env * constr * constr | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types + | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option -type position_reporting = (position * int) * EConstr.t +type position_reporting = (position * int) * constr -type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option -type type_error = (EConstr.constr, EConstr.types) ptype_error +type type_error = (constr, types) ptype_error type pretype_error = (** Old Case *) - | CantFindCaseType of EConstr.constr + | CantFindCaseType of constr (** Type inference unification *) - | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error + | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * EConstr.constr + | UnifOccurCheck of existential_key * constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option - | CannotUnify of EConstr.constr * EConstr.constr * unification_error option - | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr - | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr - | NoOccurrenceFound of EConstr.constr * Id.t option - | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option - | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types + | CannotUnify of constr * constr * unification_error option + | CannotUnifyLocal of constr * constr * constr + | CannotUnifyBindingType of Constr.constr * Constr.constr + | CannotGeneralize of Constr.constr + | NoOccurrenceFound of constr * Id.t option + | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t - | NonLinearUnification of Name.t * EConstr.constr + | NonLinearUnification of Name.t * constr (** Pretyping *) | VarNotFound of Id.t - | UnexpectedType of EConstr.constr * EConstr.constr - | NotProduct of EConstr.constr + | UnexpectedType of constr * constr + | NotProduct of constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of @@ -67,85 +68,85 @@ val precatchable_exception : exn -> bool (** Raising errors *) val error_actual_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> unification_error -> 'b val error_actual_type_core : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional : ?loc:Loc.t -> env -> Evd.evar_map -> - EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b + unsafe_judgment -> unsafe_judgment array -> 'b val error_cant_apply_bad_type : - ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr -> - EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment array -> 'b val error_case_not_inductive : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_ill_formed_branch : ?loc:Loc.t -> env -> Evd.evar_map -> - EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b + constr -> pconstructor -> constr -> constr -> 'b val error_number_branches : ?loc:Loc.t -> env -> Evd.evar_map -> - EConstr.unsafe_judgment -> int -> 'b + unsafe_judgment -> int -> 'b val error_ill_typed_rec_body : ?loc:Loc.t -> env -> Evd.evar_map -> - int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b + int -> Name.t array -> unsafe_judgment array -> types array -> 'b val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> - pinductive -> sorts_family list -> EConstr.constr -> - EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b + pinductive -> sorts_family list -> constr -> + unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b val error_not_a_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_assumption : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b -val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b +val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> EConstr.constr -> 'b +val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_unsolvable_implicit : ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> - ?reason:unification_error -> EConstr.constr * EConstr.constr -> 'b + ?reason:unification_error -> constr * constr -> 'b -val error_cannot_unify_local : env -> Evd.evar_map -> EConstr.constr * EConstr.constr * EConstr.constr -> 'b +val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - EConstr.constr -> EConstr.constr list -> (env * type_error) option -> 'b + constr -> constr list -> (env * type_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> - Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b + Name.t -> constr -> types -> types -> 'b val error_abstraction_over_meta : env -> Evd.evar_map -> metavariable -> metavariable -> 'b val error_non_linear_unification : env -> Evd.evar_map -> - metavariable -> EConstr.constr -> 'b + metavariable -> constr -> 'b (** {6 Ml Case errors } *) val error_cant_find_case_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b val error_not_product : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to glob_constr } *) -- cgit v1.2.3 From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- pretyping/pretype_errors.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/pretype_errors.mli') diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 7cef14339b..c303d5d949 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -45,8 +45,8 @@ type pretype_error = | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr - | CannotUnifyBindingType of Constr.constr * Constr.constr - | CannotGeneralize of Constr.constr + | CannotUnifyBindingType of constr * constr + | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option | WrongAbstractionType of Name.t * constr * types * types -- cgit v1.2.3