diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c3c551934..00f1760c2 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -308,7 +308,7 @@ type program_info_aux = { prg_body: constr; prg_type: constr; prg_ctx: UState.t; - prg_univdecl: Univdecls.universe_decl; + prg_univdecl: UState.universe_decl; prg_obligations: obligations; prg_deps : Id.t list; prg_fixkind : fixpoint_kind option ; @@ -615,7 +615,7 @@ let shrink_body c ty = let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = - Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst) + Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) let it_mkLambda_or_LetIn_or_clean t ctx = let open Context.Rel.Declaration in @@ -961,7 +961,7 @@ and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in let obls, rem = prg.prg_obligations in - if num < Array.length obls then + if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with None -> solve_obligation prg num tac @@ -1098,7 +1098,7 @@ let show_term n = Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env env sigma prg.prg_body) -let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl) +let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = let sign = Decls.initialize_named_context_for_proof () in @@ -1118,7 +1118,7 @@ let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl) | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic +let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = let sign = Decls.initialize_named_context_for_proof () in |