diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index ba08aa2b94..f454c389dc 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst Impargs.maybe_declare_manual_implicits false cst impargs; instance_hook pri global cst -let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = +let declare_instance_program pm env sigma ~global ~poly name pri impargs udecl term termtype = let hook { Declare.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in let pri = intern_info pri in @@ -349,9 +349,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term Decls.IsDefinition Decls.Instance in let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in - let _ : Declare.Obls.progress = - Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls - in () + let pm, _ = + Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls + in pm let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -493,7 +493,7 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp Pretyping.check_evars_are_solved ~program_mode:false env sigma; declare_instance_constant pri global imps ?hook id decl poly sigma term termtype -let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = +let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = let term, termtype, sigma = match opt_props with | Some props -> @@ -506,9 +506,10 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri term, termtype, sigma in let termtype, sigma = do_instance_resolve_TC termtype sigma env in if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then - declare_instance_constant pri global imps ?hook id decl poly sigma term termtype + let () = declare_instance_constant pri global imps ?hook id decl poly sigma term termtype in + pm else - declare_instance_program env sigma ~global ~poly id pri imps decl term termtype + declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in @@ -564,15 +565,16 @@ let new_instance_interactive ?(global=false) id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props -let new_instance_program ?(global=false) +let new_instance_program ?(global=false) ~pm ~poly instid ctx cl opt_props ?(generalize=true) ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:true ~generalize env instid ctx cl in - do_instance_program env env' sigma ?hook ~global ~poly - cty k u ctx ctx' pri decl imps subst id opt_props; - id + let pm = + do_instance_program ~pm env env' sigma ?hook ~global ~poly + cty k u ctx ctx' pri decl imps subst id opt_props in + pm, id let new_instance ?(global=false) ~poly instid ctx cl props |