diff options
| author | Pierre-Marie Pédrot | 2016-11-10 11:39:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:27 +0100 |
| commit | c2855a3387be134d1220f301574b743572a94239 (patch) | |
| tree | 441b773053d953ccc38f555c1f45e524411663d9 /pretyping/pretype_errors.ml | |
| parent | 85ab3e298aa1d7333787c1fa44d25df189ac255c (diff) | |
Unification API using EConstr.
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index c14d815054..14b25ab368 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -29,7 +29,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 *) @@ -37,17 +37,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 |