diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index c354c7d32..0a10cfdc3 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -20,6 +20,7 @@ open Libnames open Globnames open Constrintern open Constrexpr +open Sigma.Notations (*i*) open Decl_kinds @@ -322,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Proofview.Refine.refine (fun evm -> evm, Option.get term); + Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) }; Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] |