diff options
| author | Pierre-Marie Pédrot | 2016-11-07 13:27:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:26:40 +0100 |
| commit | 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 (patch) | |
| tree | a9567a1cc4be9d0625efcb94b021b4729429c0bd /ltac | |
| parent | b77579ac873975a15978c5a4ecf312d577746d26 (diff) | |
Typeclasses API using EConstr.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 5703687c48..0091d0d0a8 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -127,7 +127,7 @@ let app_poly_sort b = let find_class_proof proof_type proof_method env evars carrier relation = try let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in - let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in + let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) (EConstr.of_constr goal) in if extends_undefined (goalevars evars) evars' then raise Not_found else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] with e when Logic.catchable_exception e -> raise Not_found @@ -367,7 +367,7 @@ end) = struct let evars, inst = app_poly env (evars,Evar.Set.empty) rewrite_relation_class [| evar; mkApp (c, params) |] in - let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in + let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) (EConstr.of_constr inst) in Some (it_mkProd_or_LetIn t rels) with e when CErrors.noncritical e -> None) | _ -> None @@ -1937,7 +1937,7 @@ let default_morphism sign m = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in - let evars, mor = resolve_one_typeclass env (goalevars evars) morph in + let evars, mor = resolve_one_typeclass env (goalevars evars) (EConstr.of_constr morph) in mor, proper_projection mor morph let add_setoid global binders a aeq t n = |