diff options
| -rw-r--r-- | dev/printers.mllib | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 2 | ||||
| -rw-r--r-- | pretyping/proofview.ml | 11 | ||||
| -rw-r--r-- | pretyping/proofview.mli | 3 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 |
5 files changed, 17 insertions, 7 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index c46f6b72a..db86bb5ed 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -141,6 +141,9 @@ Find_subterm Tacred Classops Typeclasses_errors +Logic_monad +Proofview_monad +Proofview Typeclasses Detyping Indrec @@ -181,9 +184,6 @@ Refiner Clenv Evar_refiner Proof_errors -Logic_monad -Proofview_monad -Proofview Refine Proof Proof_global diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 5dfdd0379..b0d5a1df6 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -20,8 +20,8 @@ Patternops Constr_matching Tacred Typeclasses_errors -Typeclasses Proofview +Typeclasses Classops Program Coercion diff --git a/pretyping/proofview.ml b/pretyping/proofview.ml index 20be02e76..ba664cafa 100644 --- a/pretyping/proofview.ml +++ b/pretyping/proofview.ml @@ -56,10 +56,12 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) +let typeclass_resolvable = Evd.Store.field () + let dependent_init = (* Goals are created with a store which marks them as unresolvable for type classes. *) - let store = Typeclasses.set_resolvable Evd.Store.empty false in + let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) let src = (Loc.ghost,Evar_kinds.GoalEvar) in (* Main routine *) @@ -908,11 +910,16 @@ module Unsafe = struct | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x | loc,_ -> loc,Evar_kinds.GoalEvar } in - let info = Typeclasses.mark_unresolvable info in + let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with + | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } + | Some () -> info + in Evd.add evd content info let advance = advance + let typeclass_resolvable = typeclass_resolvable + end module UnsafeRepr = Proof.Unsafe diff --git a/pretyping/proofview.mli b/pretyping/proofview.mli index 6bc2e9a0e..7996b7969 100644 --- a/pretyping/proofview.mli +++ b/pretyping/proofview.mli @@ -413,6 +413,9 @@ module Unsafe : sig into [g']). It returns [None] if [g] has been (partially) solved. *) val advance : Evd.evar_map -> Evar.t -> Evar.t option + + val typeclass_resolvable : unit Evd.Store.field + end (** This module gives access to the innards of the monad. Its use is diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 0faa35c87..3a5796fe1 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -490,7 +490,7 @@ let is_instance = function Nota: we will only check the resolvability status of undefined evars. *) -let resolvable = Store.field () +let resolvable = Proofview.Unsafe.typeclass_resolvable let set_resolvable s b = if b then Store.remove s resolvable |