From 2378b5ccee0e62d0b93935aa69c0bfedd2ac720e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 11 Sep 2014 18:17:08 +0200 Subject: Add a flag for restricting resolution of typeclasses to matching (i.e. no instanciation of the goal evars). Classes defined when [Set Typeclasses Strict Resolution] is on use the restricted resolution for all their instances (except for Hint Extern's). --- pretyping/typeclasses.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 7c3d2be09..b1f816e65 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -34,6 +34,9 @@ type typeclass = { no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) cl_projs : (Name.t * (direction * int option) option * constant option) list; + + (** Whether we use matching or full unification during resolution *) + cl_strict : bool; } type instance -- cgit v1.2.3