diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index a580fd25d..25d893bfb 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -54,7 +54,7 @@ let _ = let open Vernacexpr in { info with hint_pattern = Option.map - (Constrintern.intern_constr_pattern (Global.env())) + (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env()))) info.hint_pattern } in Flags.silently (fun () -> Hints.add_hints local [typeclasses_db] @@ -336,7 +336,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let init_refine = Tacticals.New.tclTHENLIST [ Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); - Proofview.Unsafe.tclNEWGOALS gls; + Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); Tactics.New.reduce_after_refine; ] in |