diff options
| author | Gaëtan Gilbert | 2019-02-22 17:44:43 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-25 14:08:25 +0100 |
| commit | 46665f87bbdd2d5fe0c302eae63912d6418d7207 (patch) | |
| tree | 9e845e7a9358ba5442c8508036926596e6e56d8c /pretyping | |
| parent | fc76c77ac6e509c1bccc2823ce2037d21a53276a (diff) | |
Fix #9631: Instance: anomaly grounding non evar-free term
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 8 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 8 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 7 |
3 files changed, 13 insertions, 10 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d732544c5c..1496712bbc 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -124,12 +124,14 @@ let typeclass_univ_instance (cl, u) = let class_info c = try GlobRef.Map.find c !classes - with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c)) + with Not_found -> + let env = Global.env() in + not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = try let gr, u = Termops.global_of_constr sigma c in - class_info gr, u - with Not_found -> not_a_class env c + GlobRef.Map.find gr !classes, u + with Not_found -> not_a_class env sigma c let dest_class_app env sigma c = let cl, args = EConstr.decompose_app sigma c in diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 2720a3e4de..af5b3016c9 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -20,10 +20,10 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * lident (* Class name, method *) -exception TypeClassError of env * typeclass_error +exception TypeClassError of env * Evd.evar_map * typeclass_error -let typeclass_error env err = raise (TypeClassError (env, err)) +let typeclass_error env sigma err = raise (TypeClassError (env, sigma, err)) -let not_a_class env c = typeclass_error env (NotAClass c) +let not_a_class env sigma c = typeclass_error env sigma (NotAClass c) -let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) +let unbound_method env sigma cid id = typeclass_error env sigma (UnboundMethod (cid, id)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 9831627a9a..fd75781ed5 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -18,9 +18,10 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * lident (** Class name, method *) -exception TypeClassError of env * typeclass_error +exception TypeClassError of env * Evd.evar_map * typeclass_error -val not_a_class : env -> constr -> 'a +val typeclass_error : env -> Evd.evar_map -> typeclass_error -> 'a -val unbound_method : env -> GlobRef.t -> lident -> 'a +val not_a_class : env -> Evd.evar_map -> constr -> 'a +val unbound_method : env -> Evd.evar_map -> GlobRef.t -> lident -> 'a |