diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 18 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 |
2 files changed, 4 insertions, 17 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 09b2e59cea..43a450ea71 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -886,20 +886,6 @@ let pr_hint_term env sigma ctx = function let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in pr_econstr_env env sigma c -(** We need an object to record the side-effect of registering - global universes associated with a hint. *) -let cache_context_set (_,c) = - Global.push_context_set false c - -let input_context_set : Univ.ContextSet.t -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe context") with - cache_function = cache_context_set; - load_function = (fun _ -> cache_context_set); - discharge_function = (fun (_,a) -> Some a); - classify_function = (fun a -> Keep a) } - let warn_polymorphic_hint = CWarnings.create ~name:"polymorphic-hint" ~category:"automation" (fun hint -> strbrk"Using polymorphic hint " ++ hint ++ @@ -919,7 +905,7 @@ let fresh_global_or_constr env sigma poly cr = else begin if isgr then warn_polymorphic_hint (pr_hint_term env sigma ctx cr); - Lib.add_anonymous_leaf (input_context_set ctx); + Declare.declare_universe_context false ctx; (c, Univ.ContextSet.empty) end @@ -1315,7 +1301,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) - else (Lib.add_anonymous_leaf (input_context_set diff); + else (Declare.declare_universe_context false diff; IsConstr (c', Univ.ContextSet.empty)) let project_hint ~poly pri l2r r = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5fc34619e8..2a8ebe08ca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5063,6 +5063,7 @@ let constr_eq ~strict x y = let unify ?(state=full_transparent_state) x y = Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in try let core_flags = @@ -5078,7 +5079,7 @@ let unify ?(state=full_transparent_state) x y = let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in Proofview.Unsafe.tclEVARS sigma with e when CErrors.noncritical e -> - Tacticals.New.tclFAIL 0 (str"Not unifiable") + Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None))) end module Simple = struct |