diff options
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 2 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 10 | ||||
| -rw-r--r-- | vernac/declare.ml | 654 | ||||
| -rw-r--r-- | vernac/declare.mli | 172 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 645 | ||||
| -rw-r--r-- | vernac/declareObl.mli | 175 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 2 | ||||
| -rw-r--r-- | vernac/locality.ml | 12 | ||||
| -rw-r--r-- | vernac/locality.mli | 5 | ||||
| -rw-r--r-- | vernac/obligations.ml | 14 | ||||
| -rw-r--r-- | vernac/obligations.mli | 6 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
16 files changed, 846 insertions, 868 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index aa5a14c7dd..177a76e64b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - DeclareObl.State.prg_tag + Declare.Obls.State.prg_tag type cached_state = | EmptyState @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.State.t + Declare.Obls.State.t type partial_state = [ `Full of Vernacstate.t @@ -3308,7 +3308,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/vernac/classes.ml b/vernac/classes.ml index 55af2e1a7d..21e2afe6a9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -345,7 +345,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in - let _ : DeclareObl.progress = + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 95f3955309..eac8f92e2e 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,7 +127,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in - let _ : DeclareObl.progress = + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls in () diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4e9e24b119..4aa46e0a86 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive ~scope ~poly fixkind fixl = - let cofix = fixkind = DeclareObl.IsCoFixpoint in + let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl in @@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = end in let uctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> Decls.Fixpoint - | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint + | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint + | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind @@ -345,7 +345,7 @@ let do_fixpoint ~scope ~poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let annots = List.map (fun fix -> Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in - let fixkind = DeclareObl.IsFixpoint annots in + let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in do_program_recursive ~scope ~poly fixkind l @@ -355,4 +355,4 @@ let do_fixpoint ~scope ~poly l = let do_cofixpoint ~scope ~poly fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl + do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl diff --git a/vernac/declare.ml b/vernac/declare.ml index c3f95c5297..a34b069f2f 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -120,7 +120,7 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type import_status = ImportDefaultBehavior | ImportNeedQualified +type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) @@ -876,7 +876,7 @@ let _ = Abstract.declare_abstract := declare_abstract let declare_universe_context = DeclareUctx.declare_universe_context -type locality = Discharge | Global of import_status +type locality = Locality.locality = | Discharge | Global of import_status (* Hooks naturally belong here as they apply to both definitions and lemmas *) module Hook = struct @@ -1053,3 +1053,653 @@ let prepare_parameter ~poly ~udecl ~types sigma = (* Compat: will remove *) exception AlreadyDeclared = DeclareUniv.AlreadyDeclared + +module Obls = struct + +open Constr + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +module Obligation = struct + type t = + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + + let set_type ~typ obl = {obl with obl_type = typ} + let set_body ~body obl = {obl with obl_body = Some body} +end + +type obligations = {obls : Obligation.t array; remaining : int} +type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint + +module ProgramDecl = struct + type t = + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : Hook.t option + ; prg_opaque : bool } + + open Obligation + + let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs ~poly ~scope ~kind b + t deps fixkind notations obls reduce = + let obls', b = + match b with + | None -> + assert (Int.equal (Array.length obls) 0); + let n = Nameops.add_suffix n "_obligation" in + ( [| { obl_name = n + ; obl_body = None + ; obl_location = Loc.tag Evar_kinds.InternalHole + ; obl_type = t + ; obl_status = (false, Evar_kinds.Expand) + ; obl_deps = Int.Set.empty + ; obl_tac = None } |] + , mkVar n ) + | Some b -> + ( Array.mapi + (fun i (n, t, l, o, d, tac) -> + { obl_name = n + ; obl_body = None + ; obl_location = l + ; obl_type = t + ; obl_status = o + ; obl_deps = d + ; obl_tac = tac }) + obls + , b ) + in + let ctx = UState.make_flexible_nonalgebraic uctx in + { prg_name = n + ; prg_body = b + ; prg_type = reduce t + ; prg_ctx = ctx + ; prg_univdecl = udecl + ; prg_obligations = {obls = obls'; remaining = Array.length obls'} + ; prg_deps = deps + ; prg_fixkind = fixkind + ; prg_notations = notations + ; prg_implicits = impargs + ; prg_poly = poly + ; prg_scope = scope + ; prg_kind = kind + ; prg_reduce = reduce + ; prg_hook = hook + ; prg_opaque = opaque } + + let set_uctx ~uctx prg = {prg with prg_ctx = uctx} +end + +open Obligation +open ProgramDecl + +(* Saving an obligation *) + +(* XXX: Is this the right place for this? *) +let it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then Term.mkLambda_or_LetIn decl t + else if Vars.noccurn 1 t then Vars.subst1 mkProp t + else Term.mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + +(* XXX: Is this the right place for this? *) +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match (Constr.kind c, Constr.kind ty) with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when Constr.equal b b' && Constr.equal t t' -> + let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in + aux ctx' c ty + | _, LetIn (x', b', t', ty) -> + let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in + aux ctx' (lift 1 c) ty + | LetIn (x, b, t, c), _ -> + let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in + aux ctx' c (lift 1 ty) + | Lambda (x, b, t), Prod (x', b', t') + (* By invariant, must be convertible *) -> + let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in + aux ctx' t t' + | Cast (c, _, _), _ -> aux ctx c ty + | _, _ -> (ctx, c, ty) + in + aux Context.Rel.empty c ty + +(* XXX: What's the relation of this with Abstract.shrink ? *) +let shrink_body c ty = + let ctx, b, ty = + match ty with + | None -> + let ctx, b = Term.decompose_lam_assum c in + (ctx, b, None) + | Some ty -> + let ctx, b, ty = decompose_lam_prod c ty in + (ctx, b, Some ty) + in + let b', ty', n, args = + List.fold_left + (fun (b, ty, i, args) decl -> + if Vars.noccurn 1 b && Option.cata (Vars.noccurn 1) true ty then + (Vars.subst1 mkProp b, Option.map (Vars.subst1 mkProp) ty, succ i, args) + else + let open Context.Rel.Declaration in + let args = if is_local_assum decl then mkRel i :: args else args in + ( Term.mkLambda_or_LetIn decl b + , Option.map (Term.mkProd_or_LetIn decl) ty + , succ i + , args )) + (b, ty, 1, []) ctx + in + (ctx, b', ty', Array.of_list args) + +(***********************************************************************) +(* Saving an obligation *) +(***********************************************************************) + +let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] + +let add_hint local prg cst = + let locality = if local then Goptions.OptLocal else Goptions.OptExport in + Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) + +(* true = hide obligations *) +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:true + ~key:["Hide"; "Obligations"] + ~value:false + +let declare_obligation prg obl body ty uctx = + let body = prg.prg_reduce body in + let ty = Option.map prg.prg_reduce ty in + match obl.obl_status with + | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) + | force, Evar_kinds.Define opaque -> + let opaque = (not force) && opaque in + let poly = prg.prg_poly in + let ctx, body, ty, args = + if not poly then shrink_body body ty + else ([], body, ty, [||]) + in + let ce = definition_entry ?types:ty ~opaque ~univs:uctx body in + (* ppedrot: seems legit to have obligations as local *) + let constant = + declare_constant ~name:obl.obl_name + ~local:ImportNeedQualified + ~kind:Decls.(IsProof Property) + (DefinitionEntry ce) + in + if not opaque then + add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = + match uctx with + | Entries.Polymorphic_entry (_, uctx) -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Entries.Monomorphic_entry _ -> + Some + (TermObl + (it_mkLambda_or_LetIn_or_clean + (mkApp (mkConst constant, args)) + ctx)) + in + (true, {obl with obl_body = body}) + +(* Updating the obligation meta-info on close *) + +let not_transp_msg = + Pp.( + str "Obligation should be transparent but was declared opaque." + ++ spc () + ++ str "Use 'Defined' instead.") + +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd +let err_not_transp () = pperror not_transp_msg + +module ProgMap = Id.Map + +module StateFunctional = struct + + type t = ProgramDecl.t CEphemeron.key ProgMap.t + + let _empty = ProgMap.empty + + let pending pm = + ProgMap.filter + (fun _ v -> (CEphemeron.get v).prg_obligations.remaining > 0) + pm + + let num_pending pm = pending pm |> ProgMap.cardinal + + let first_pending pm = + pending pm |> ProgMap.choose_opt + |> Option.map (fun (_, v) -> CEphemeron.get v) + + let get_unique_open_prog pm name : (_, Id.t list) result = + match name with + | Some n -> + Option.cata + (fun p -> Ok (CEphemeron.get p)) + (Error []) (ProgMap.find_opt n pm) + | None -> ( + let n = num_pending pm in + match n with + | 0 -> Error [] + | 1 -> Option.cata (fun p -> Ok p) (Error []) (first_pending pm) + | _ -> + let progs = Id.Set.elements (ProgMap.domain pm) in + Error progs ) + + let add t key prg = ProgMap.add key (CEphemeron.create prg) t + + let fold t ~f ~init = + let f k v acc = f k (CEphemeron.get v) acc in + ProgMap.fold f t init + + let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v) + let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get +end + +module State = struct + + type t = StateFunctional.t + + open StateFunctional + + let prg_ref, prg_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" + + let num_pending () = num_pending !prg_ref + let first_pending () = first_pending !prg_ref + let get_unique_open_prog id = get_unique_open_prog !prg_ref id + let add id prg = prg_ref := add !prg_ref id prg + let fold ~f ~init = fold !prg_ref ~f ~init + let all () = all !prg_ref + let find id = find !prg_ref id + +end + +(* In all cases, the use of the map is read-only so we don't expose the ref *) +let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] + +let check_solved_obligations ~what_for : unit = + if not (ProgMap.is_empty !State.prg_ref) then + let keys = map_keys !State.prg_ref in + let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in + CErrors.user_err ~hdr:"Program" + Pp.( + str "Unsolved obligations when closing " + ++ what_for ++ str ":" ++ spc () + ++ prlist_with_sep spc (fun x -> Id.print x) keys + ++ str have_string + ++ str "unsolved obligations" ) + +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) +let progmap_remove pm prg = ProgMap.remove prg.prg_name pm +let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm +let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 + +let obligations_message rem = + Format.asprintf "%s %s remaining" + (if rem > 0 then string_of_int rem else "No more") + (CString.plural rem "obligation") + |> Pp.str |> Flags.if_verbose Feedback.msg_info + +type progress = Remain of int | Dependent | Defined of GlobRef.t + +let get_obligation_body expand obl = + match obl.obl_body with + | None -> None + | Some c -> ( + if expand && snd obl.obl_status == Evar_kinds.Expand then + match c with + | DefinedObl pc -> Some (Environ.constant_value_in (Global.env ()) pc) + | TermObl c -> Some c + else + match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) + +let obl_substitution expand obls deps = + Int.Set.fold + (fun x acc -> + let xobl = obls.(x) in + match get_obligation_body expand xobl with + | None -> acc + | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) + deps [] + +let rec intset_to = function + | -1 -> Int.Set.empty + | n -> Int.Set.add n (intset_to (pred n)) + +let obligation_substitution expand prg = + let obls = prg.prg_obligations.obls in + let ints = intset_to (pred (Array.length obls)) in + obl_substitution expand obls ints + +let hide_obligation () = + Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; + UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref "program.tactics.obligation") + +(* XXX: Is this the right place? *) +let rec prod_app t n = + match + Constr.kind + (EConstr.Unsafe.to_constr + (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) + (* FIXME *) + with + | Prod (_, _, b) -> Vars.subst1 n b + | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n + | _ -> + CErrors.user_err ~hdr:"prod_app" + Pp.(str "Needed a product, but didn't find one" ++ fnl ()) + +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL + +let replace_appvars subst = + let rec aux c = + let f, l = decompose_app c in + if isVar f then + try + let c' = List.map (Constr.map aux) l in + let t, b = Id.List.assoc (destVar f) subst in + mkApp + ( delayed_force hide_obligation + , [|prod_applist t c'; Term.applistc b c'|] ) + with Not_found -> Constr.map aux c + else Constr.map aux c + in + Constr.map aux + +let subst_prog subst prg = + if get_hide_obligations () then + ( replace_appvars subst prg.prg_body + , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) + else + let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in + ( Vars.replace_vars subst' prg.prg_body + , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) + +let stm_get_fix_exn = ref (fun _ x -> x) + +let declare_definition prg = + let varsubst = obligation_substitution true prg in + let sigma = Evd.from_ctx prg.prg_ctx in + let body, types = subst_prog varsubst prg in + let body, types = EConstr.(of_constr body, Some (of_constr types)) in + (* All these should be grouped into a struct a some point *) + let opaque, poly, udecl, hook = + (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook) + in + let name, scope, kind, impargs = + ( prg.prg_name + , prg.prg_scope + , Decls.(IsDefinition prg.prg_kind) + , prg.prg_implicits ) + in + let fix_exn = !stm_get_fix_exn () in + let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in + (* XXX: This is doing normalization twice *) + let kn = + declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + in + let pm = progmap_remove !State.prg_ref prg in + State.prg_ref := pm; + kn + +let rec lam_index n t acc = + match Constr.kind t with + | Lambda ({Context.binder_name = Name n'}, _, _) when Id.equal n n' -> acc + | Lambda (_, _, b) -> lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences n fixbody fixtype = + match n with + | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in + let ctx = fst (Term.decompose_prod_n_assum m fixtype) in + List.map_i (fun i _ -> i) 0 ctx + +let declare_mutual_definition l = + let len = List.length l in + let first = List.hd l in + let defobl x = + let oblsubst = obligation_substitution true x in + let subs, typ = subst_prog oblsubst x in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in + let term = + snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) + in + let typ = + snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) + in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in + let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in + (def, oblsubst) + in + let defs, obls = + List.fold_right + (fun x (defs, obls) -> + let xdef, xobls = defobl x in + (xdef :: defs, xobls @ obls)) + l ([], []) + in + (* let fixdefs = List.map reduce_fix fixdefs in *) + let fixdefs, fixrs, fixtypes, fixitems = + List.fold_right2 + (fun (d, r, typ, impargs) name (a1, a2, a3, a4) -> + ( d :: a1 + , r :: a2 + , typ :: a3 + , Recthm.{name; typ; impargs; args = []} :: a4 )) + defs first.prg_deps ([], [], [], []) + in + let fixkind = Option.get first.prg_fixkind in + let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in + let rvec = Array.of_list fixrs in + let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in + let rec_declaration = (Array.map2 Context.make_annot namevec rvec, arrrec, recvec) in + let possible_indexes = + match fixkind with + | IsFixpoint wfl -> + Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) + | IsCoFixpoint -> None + in + (* In the future we will pack all this in a proper record *) + let poly, scope, ntns, opaque = + (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque) + in + let kind = + if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) + else Decls.(IsDefinition CoFixpoint) + in + (* Declare the recursive definitions *) + let udecl = UState.default_univ_decl in + let kns = + declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns + ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly + ~restrict_ucontext:false fixitems + in + (* Only for the first constant *) + let dref = List.hd kns in + Hook.( + call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref}); + let pm = List.fold_left progmap_remove !State.prg_ref l in + State.prg_ref := pm; + dref + +let update_obls prg obls rem = + let prg_obligations = {obls; remaining = rem} in + let prg' = {prg with prg_obligations} in + let pm = progmap_replace prg' !State.prg_ref in + State.prg_ref := pm; + obligations_message rem; + if rem > 0 then Remain rem + else + match prg'.prg_deps with + | [] -> + let kn = declare_definition prg' in + let pm = progmap_remove !State.prg_ref prg' in + State.prg_ref := pm; + Defined kn + | l -> + let progs = + List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps + in + if List.for_all (fun x -> obligations_solved x) progs then + let kn = declare_mutual_definition progs in + Defined kn + else Dependent + +let dependencies obls n = + let res = ref Int.Set.empty in + Array.iteri + (fun i obl -> + if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then + res := Int.Set.add i !res) + obls; + !res + +let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = + let obls = Array.copy obls in + let () = obls.(num) <- obl in + let prg = {prg with prg_ctx = uctx} in + let _progress = update_obls prg obls (pred rem) in + let () = + if pred rem > 0 then + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + let _progress = auto (Some prg.prg_name) deps None in + () + else () + else () + in + () + +type obligation_resolver = + Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> progress + +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +let obligation_terminator entries uctx {name; num; auto} = + match entries with + | [entry] -> + let env = Global.env () in + let ty = entry.proof_entry_type in + let body, uctx = inline_private_constants ~uctx env entry in + let sigma = Evd.from_ctx uctx in + Inductiveops.control_only_guard (Global.env ()) sigma + (EConstr.of_constr body); + (* Declare the obligation ourselves and drop the hook *) + let prg = Option.get (State.find name) in + let {obls; remaining = rem} = prg.prg_obligations in + let obl = obls.(num) in + let status = + match (obl.obl_status, entry.proof_entry_opaque) with + | (_, Evar_kinds.Expand), true -> err_not_transp () + | (true, _), true -> err_not_transp () + | (false, _), true -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), false -> Evar_kinds.Define false + | (_, status), false -> status + in + let obl = {obl with obl_status = (false, status)} in + let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in + let defined, obl = declare_obligation prg obl body ty univs in + let prg_ctx = + if prg.prg_poly then + (* Polymorphic *) + (* We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx uctx + else if + (* The first obligation, if defined, + declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + defined + then + UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) + else uctx + in + update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto + | _ -> + CErrors.anomaly + Pp.( + str + "[obligation_terminator] close_proof returned more than one proof \ + term") + +(* Similar to the terminator but for the admitted path; this assumes + the admitted constant was already declared. + + FIXME: There is duplication of this code with obligation_terminator + and Obligations.admit_obligations *) +let obligation_admitted_terminator {name; num; auto} ctx' dref = + let prg = Option.get (State.find name) in + let {obls; remaining = rem} = prg.prg_obligations in + let obl = obls.(num) in + let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in + let transparent = Environ.evaluable_constant cst (Global.env ()) in + let () = + match obl.obl_status with + | true, Evar_kinds.Expand | true, Evar_kinds.Define true -> + if not transparent then err_not_transp () + | _ -> () + in + let inst, ctx' = + if not prg.prg_poly (* Not polymorphic *) then + (* The universe context was declared globally, we continue + from the new global environment. *) + let ctx = + UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) + in + let ctx' = UState.merge_subst ctx (UState.subst ctx') in + (Univ.Instance.empty, ctx') + else + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in + (Univ.UContext.instance uctx, ctx') + in + let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in + let () = if transparent then add_hint true prg cst in + update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto + +end diff --git a/vernac/declare.mli b/vernac/declare.mli index 340c035d1d..2c4a801f9a 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -160,7 +160,7 @@ val definition_entry -> constr -> Evd.side_effects proof_entry -type import_status = ImportDefaultBehavior | ImportNeedQualified +type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -177,17 +177,6 @@ val declare_constant -> Evd.side_effects constant_entry -> Constant.t -(** [inline_private_constants ~sideff ~uctx env ce] will inline the - constants in [ce]'s body and return the body plus the updated - [UState.t]. - - XXX: Scheduled for removal from public API, don't rely on it *) -val inline_private_constants - : uctx:UState.t - -> Environ.env - -> Evd.side_effects proof_entry - -> Constr.t * UState.t - (** Declaration messages *) (** XXX: Scheduled for removal from public API, do not use *) @@ -233,6 +222,7 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Returns [false] if an unsafe tactic has been used. *) val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool +(** Semantics of this function is a bit dubious, use with care *) val build_by_tactic : ?side_eff:bool -> Environ.env @@ -260,7 +250,7 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env environment and empty evar_map. *) val get_current_context : Proof.t -> Evd.evar_map * Environ.env -(** Temporarily re-exported for 3rd party code; don't use *) +(** XXX: Temporarily re-exported for 3rd party code; don't use *) val build_constant_by_tactic : name:Names.Id.t -> ?opaque:opacity_flag -> @@ -274,7 +264,7 @@ val build_constant_by_tactic : val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] -type locality = Discharge | Global of import_status +type locality = Locality.locality = Discharge | Global of import_status (** Declaration hooks *) module Hook : sig @@ -397,3 +387,157 @@ val prepare_parameter (* Compat: will remove *) exception AlreadyDeclared of (string option * Names.Id.t) + +module Obls : sig + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +module Obligation : sig + type t = private + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + + val set_type : typ:Constr.types -> t -> t + val set_body : body:pconstant obligation_body -> t -> t +end + +type obligations = {obls : Obligation.t array; remaining : int} +type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint + +(* Information about a single [Program {Definition,Lemma,..}] declaration *) +module ProgramDecl : sig + type t = private + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : Hook.t option + ; prg_opaque : bool } + + val make : + ?opaque:bool + -> ?hook:Hook.t + -> Names.Id.t + -> udecl:UState.universe_decl + -> uctx:UState.t + -> impargs:Impargs.manual_implicits + -> poly:bool + -> scope:locality + -> kind:Decls.definition_object_kind + -> Constr.constr option + -> Constr.types + -> Names.Id.t list + -> fixpoint_kind option + -> Vernacexpr.decl_notation list + -> ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array + -> (Constr.constr -> Constr.constr) + -> t + + val set_uctx : uctx:UState.t -> t -> t +end + +(** [declare_obligation] Save an obligation *) +val declare_obligation : + ProgramDecl.t + -> Obligation.t + -> Constr.types + -> Constr.types option + -> Entries.universes_entry + -> bool * Obligation.t + +module State : sig + + val num_pending : unit -> int + val first_pending : unit -> ProgramDecl.t option + + (** Returns [Error duplicate_list] if not a single program is open *) + val get_unique_open_prog : + Id.t option -> (ProgramDecl.t, Id.t list) result + + (** Add a new obligation *) + val add : Id.t -> ProgramDecl.t -> unit + + val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a + + val all : unit -> ProgramDecl.t list + + val find : Id.t -> ProgramDecl.t option + + (* Internal *) + type t + val prg_tag : t Summary.Dyn.tag +end + +val declare_definition : ProgramDecl.t -> Names.GlobRef.t + +(** Resolution status of a program *) +type progress = + | Remain of int (** n obligations remaining *) + | Dependent (** Dependent on other definitions *) + | Defined of GlobRef.t (** Defined as id *) + +type obligation_resolver = + Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> progress + +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +(** [obligation_terminator] part 2 of saving an obligation, proof mode *) +val obligation_terminator : + Evd.side_effects proof_entry list + -> UState.t + -> obligation_qed_info + -> unit + +(** [obligation_admitted_terminator] part 2 of saving an obligation, non-interactive mode *) +val obligation_admitted_terminator : + obligation_qed_info -> UState.t -> GlobRef.t -> unit + +(** [update_obls prg obls n progress] What does this do? *) +val update_obls : + ProgramDecl.t -> Obligation.t array -> int -> progress + +(** Check obligations are properly solved before closing the + [what_for] section / module *) +val check_solved_obligations : what_for:Pp.t -> unit + +(** { 2 Util } *) + +val obl_substitution : + bool + -> Obligation.t array + -> Int.Set.t + -> (Id.t * (Constr.types * Constr.types)) list + +val dependencies : Obligation.t array -> int -> Int.Set.t +val err_not_transp : unit -> unit + +(* This is a hack to make it possible for Obligations to craft a Qed + * behind the scenes. The fix_exn the Stm attaches to the Future proof + * is not available here, so we provide a side channel to get it *) +val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref + +end diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml deleted file mode 100644 index b2f9383f8c..0000000000 --- a/vernac/declareObl.ml +++ /dev/null @@ -1,645 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Names -open Environ -open Context -open Constr -open Vars -open Entries - -type 'a obligation_body = DefinedObl of 'a | TermObl of constr - -module Obligation = struct - type t = - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } - - let set_type ~typ obl = { obl with obl_type = typ } - let set_body ~body obl = { obl with obl_body = Some body } - -end - -type obligations = - { obls : Obligation.t array - ; remaining : int } - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -module ProgramDecl = struct - - type t = - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : Declare.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : Declare.Hook.t option - ; prg_opaque : bool - } - - open Obligation - - let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs - ~poly ~scope ~kind b t deps fixkind notations obls reduce = - let obls', b = - match b with - | None -> - assert(Int.equal (Array.length obls) 0); - let n = Nameops.add_suffix n "_obligation" in - [| { obl_name = n; obl_body = None; - obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; - obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; - obl_tac = None } |], - mkVar n - | Some b -> - Array.mapi - (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls, b - in - let ctx = UState.make_flexible_nonalgebraic uctx in - { prg_name = n - ; prg_body = b - ; prg_type = reduce t - ; prg_ctx = ctx - ; prg_univdecl = udecl - ; prg_obligations = { obls = obls' ; remaining = Array.length obls' } - ; prg_deps = deps - ; prg_fixkind = fixkind - ; prg_notations = notations - ; prg_implicits = impargs - ; prg_poly = poly - ; prg_scope = scope - ; prg_kind = kind - ; prg_reduce = reduce - ; prg_hook = hook - ; prg_opaque = opaque - } - - let set_uctx ~uctx prg = {prg with prg_ctx = uctx} -end - -open Obligation -open ProgramDecl - -(* Saving an obligation *) - -(* XXX: Is this the right place for this? *) -let it_mkLambda_or_LetIn_or_clean t ctx = - let open Context.Rel.Declaration in - let fold t decl = - if is_local_assum decl then Term.mkLambda_or_LetIn decl t - else if noccurn 1 t then subst1 mkProp t - else Term.mkLambda_or_LetIn decl t - in - Context.Rel.fold_inside fold ctx ~init:t - -(* XXX: Is this the right place for this? *) -let decompose_lam_prod c ty = - let open Context.Rel.Declaration in - let rec aux ctx c ty = - match (Constr.kind c, Constr.kind ty) with - | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when Constr.equal b b' && Constr.equal t t' -> - let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in - aux ctx' c ty - | _, LetIn (x', b', t', ty) -> - let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in - aux ctx' (lift 1 c) ty - | LetIn (x, b, t, c), _ -> - let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in - aux ctx' c (lift 1 ty) - | Lambda (x, b, t), Prod (x', b', t') - (* By invariant, must be convertible *) -> - let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in - aux ctx' t t' - | Cast (c, _, _), _ -> aux ctx c ty - | _, _ -> (ctx, c, ty) - in - aux Context.Rel.empty c ty - -(* XXX: What's the relation of this with Abstract.shrink ? *) -let shrink_body c ty = - let ctx, b, ty = - match ty with - | None -> - let ctx, b = Term.decompose_lam_assum c in - (ctx, b, None) - | Some ty -> - let ctx, b, ty = decompose_lam_prod c ty in - (ctx, b, Some ty) - in - let b', ty', n, args = - List.fold_left - (fun (b, ty, i, args) decl -> - if noccurn 1 b && Option.cata (noccurn 1) true ty then - (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args) - else - let open Context.Rel.Declaration in - let args = if is_local_assum decl then mkRel i :: args else args in - ( Term.mkLambda_or_LetIn decl b - , Option.map (Term.mkProd_or_LetIn decl) ty - , succ i - , args ) ) - (b, ty, 1, []) ctx - in - (ctx, b', ty', Array.of_list args) - -(***********************************************************************) -(* Saving an obligation *) -(***********************************************************************) - -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] - -let add_hint local prg cst = - let locality = if local then Goptions.OptLocal else Goptions.OptExport in - Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) - -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true - ~key:["Hide"; "Obligations"] - ~value:false - -let declare_obligation prg obl body ty uctx = - let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in - match obl.obl_status with - | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) - | force, Evar_kinds.Define opaque -> - let opaque = (not force) && opaque in - let poly = prg.prg_poly in - let ctx, body, ty, args = - if not poly then shrink_body body ty - else ([], body, ty, [||]) - in - let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in - - (* ppedrot: seems legit to have obligations as local *) - let constant = - Declare.declare_constant ~name:obl.obl_name - ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property) - (Declare.DefinitionEntry ce) - in - if not opaque then - add_hint (Locality.make_section_locality None) prg constant; - Declare.definition_message obl.obl_name; - let body = - match uctx with - | Polymorphic_entry (_, uctx) -> - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_entry _ -> - Some - (TermObl - (it_mkLambda_or_LetIn_or_clean - (mkApp (mkConst constant, args)) - ctx)) - in - (true, {obl with obl_body = body}) - -(* Updating the obligation meta-info on close *) - -let not_transp_msg = - Pp.( - str "Obligation should be transparent but was declared opaque." - ++ spc () - ++ str "Use 'Defined' instead.") - -let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -let err_not_transp () = pperror not_transp_msg - -module ProgMap = Id.Map - -module StateFunctional = struct - - type t = ProgramDecl.t CEphemeron.key ProgMap.t - - let _empty = ProgMap.empty - - let pending pm = - ProgMap.filter - (fun _ v -> (CEphemeron.get v).prg_obligations.remaining > 0) - pm - - let num_pending pm = pending pm |> ProgMap.cardinal - - let first_pending pm = - pending pm |> ProgMap.choose_opt - |> Option.map (fun (_, v) -> CEphemeron.get v) - - let get_unique_open_prog pm name : (_, Id.t list) result = - match name with - | Some n -> - Option.cata - (fun p -> Ok (CEphemeron.get p)) - (Error []) (ProgMap.find_opt n pm) - | None -> ( - let n = num_pending pm in - match n with - | 0 -> Error [] - | 1 -> Option.cata (fun p -> Ok p) (Error []) (first_pending pm) - | _ -> - let progs = Id.Set.elements (ProgMap.domain pm) in - Error progs ) - - let add t key prg = ProgMap.add key (CEphemeron.create prg) t - - let fold t ~f ~init = - let f k v acc = f k (CEphemeron.get v) acc in - ProgMap.fold f t init - - let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v) - let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get -end - -module State = struct - - type t = StateFunctional.t - - open StateFunctional - - let prg_ref, prg_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - - let num_pending () = num_pending !prg_ref - let first_pending () = first_pending !prg_ref - let get_unique_open_prog id = get_unique_open_prog !prg_ref id - let add id prg = prg_ref := add !prg_ref id prg - let fold ~f ~init = fold !prg_ref ~f ~init - let all () = all !prg_ref - let find id = find !prg_ref id - -end - -(* In all cases, the use of the map is read-only so we don't expose the ref *) -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let check_solved_obligations ~what_for : unit = - if not (ProgMap.is_empty !State.prg_ref) then - let keys = map_keys !State.prg_ref in - let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in - CErrors.user_err ~hdr:"Program" - Pp.( - str "Unsolved obligations when closing " - ++ what_for ++ str ":" ++ spc () - ++ prlist_with_sep spc (fun x -> Id.print x) keys - ++ str have_string - ++ str "unsolved obligations" ) - -let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) -let progmap_remove pm prg = ProgMap.remove prg.prg_name pm -let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm -let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 - -let obligations_message rem = - Format.asprintf "%s %s remaining" - (if rem > 0 then string_of_int rem else "No more") - (CString.plural rem "obligation") - |> Pp.str |> Flags.if_verbose Feedback.msg_info - -type progress = Remain of int | Dependent | Defined of GlobRef.t - -let get_obligation_body expand obl = - match obl.obl_body with - | None -> None - | Some c -> ( - if expand && snd obl.obl_status == Evar_kinds.Expand then - match c with - | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) - | TermObl c -> Some c - else - match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) - -let obl_substitution expand obls deps = - Int.Set.fold - (fun x acc -> - let xobl = obls.(x) in - match get_obligation_body expand xobl with - | None -> acc - | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc ) - deps [] - -let rec intset_to = function - | -1 -> Int.Set.empty - | n -> Int.Set.add n (intset_to (pred n)) - -let obligation_substitution expand prg = - let obls = prg.prg_obligations.obls in - let ints = intset_to (pred (Array.length obls)) in - obl_substitution expand obls ints - -let hide_obligation () = - Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; - UnivGen.constr_of_monomorphic_global - (Coqlib.lib_ref "program.tactics.obligation") - -(* XXX: Is this the right place? *) -let rec prod_app t n = - match - Constr.kind - (EConstr.Unsafe.to_constr - (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) - (* FIXME *) - with - | Prod (_, _, b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - CErrors.user_err ~hdr:"prod_app" - Pp.(str "Needed a product, but didn't find one" ++ fnl ()) - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let t, b = Id.List.assoc (destVar f) subst in - mkApp - ( delayed_force hide_obligation - , [|prod_applist t c'; Term.applistc b c'|] ) - with Not_found -> Constr.map aux c - else Constr.map aux c - in - Constr.map aux - -let subst_prog subst prg = - if get_hide_obligations () then - ( replace_appvars subst prg.prg_body - , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) - else - let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in - ( Vars.replace_vars subst' prg.prg_body - , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) - -let get_fix_exn, stm_get_fix_exn = Hook.make () - -let declare_definition prg = - let varsubst = obligation_substitution true prg in - let sigma = Evd.from_ctx prg.prg_ctx in - let body, types = subst_prog varsubst prg in - let body, types = EConstr.(of_constr body, Some (of_constr types)) in - (* All these should be grouped into a struct a some point *) - let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in - let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in - let fix_exn = Hook.get get_fix_exn () in - let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in - (* XXX: This is doing normalization twice *) - let kn = - Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls - ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma - in - let pm = progmap_remove !State.prg_ref prg in - State.prg_ref := pm; - kn - -let rec lam_index n t acc = - match Constr.kind t with - | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc - | Lambda (_, _, b) -> lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences n fixbody fixtype = - match n with - | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = - Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) - (* FIXME *) - in - let ctx = fst (Term.decompose_prod_n_assum m fixtype) in - List.map_i (fun i _ -> i) 0 ctx - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let defobl x = - let oblsubst = obligation_substitution true x in - let subs, typ = subst_prog oblsubst x in - let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in - let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in - let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in - let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in - let term = EConstr.to_constr sigma term in - let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in - let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in - def, oblsubst - in - let defs, obls = - List.fold_right (fun x (defs, obls) -> - let xdef, xobls = defobl x in - (xdef :: defs, xobls @ obls)) l ([], []) - in - (* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs, fixtypes, fixitems = - List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) -> - d :: a1, r :: a2, typ :: a3, - Declare.Recthm.{ name; typ; impargs; args = [] } :: a4 - ) defs first.prg_deps ([],[],[],[]) - in - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in - let rvec = Array.of_list fixrs in - let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let possible_indexes = - match fixkind with - | IsFixpoint wfl -> - Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) - | IsCoFixpoint -> None - in - (* In the future we will pack all this in a proper record *) - let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in - (* Declare the recursive definitions *) - let udecl = UState.default_univ_decl in - let kns = - Declare.declare_mutually_recursive ~scope ~opaque ~kind - ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly - ~restrict_ucontext:false fixitems - in - (* Only for the first constant *) - let dref = List.hd kns in - Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); - let pm = List.fold_left progmap_remove !State.prg_ref l in - State.prg_ref := pm; - dref - -let update_obls prg obls rem = - let prg_obligations = { obls; remaining = rem } in - let prg' = {prg with prg_obligations} in - let pm = progmap_replace prg' !State.prg_ref in - State.prg_ref := pm; - obligations_message rem; - if rem > 0 then Remain rem - else - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - let pm = progmap_remove !State.prg_ref prg' in - State.prg_ref := pm; - Defined kn - | l -> - let progs = - List.map - (fun x -> CEphemeron.get (ProgMap.find x pm)) - prg'.prg_deps - in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent - -let dependencies obls n = - let res = ref Int.Set.empty in - Array.iteri - (fun i obl -> - if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then - res := Int.Set.add i !res ) - obls; - !res - -let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg = { prg with prg_ctx = uctx } in - let _progress = update_obls prg obls (pred rem) in - let () = - if pred rem > 0 then - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - let _progress = auto (Some prg.prg_name) deps None in - () - else () - else () - in - () - -type obligation_resolver = - Id.t option - -> Int.Set.t - -> unit Proofview.tactic option - -> progress - -type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} - -let obligation_terminator entries uctx {name; num; auto} = - match entries with - | [entry] -> - let env = Global.env () in - let ty = entry.Declare.proof_entry_type in - let body, uctx = Declare.inline_private_constants ~uctx env entry in - let sigma = Evd.from_ctx uctx in - Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); - (* Declare the obligation ourselves and drop the hook *) - let prg = Option.get (State.find name) in - let { obls; remaining=rem } = prg.prg_obligations in - let obl = obls.(num) in - let status = - match obl.obl_status, entry.Declare.proof_entry_opaque with - | (_, Evar_kinds.Expand), true -> err_not_transp () - | (true, _), true -> err_not_transp () - | (false, _), true -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), false -> - Evar_kinds.Define false - | (_, status), false -> status - in - let obl = { obl with obl_status = false, status } in - let uctx = - if prg.prg_poly then uctx - else UState.union prg.prg_ctx uctx - in - let univs = UState.univ_entry ~poly:prg.prg_poly uctx in - let (defined, obl) = declare_obligation prg obl body ty univs in - let prg_ctx = - if prg.prg_poly then (* Polymorphic *) - (* We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx uctx - else if - (* The first obligation, if defined, - declares the univs of the constant, - each subsequent obligation declares its own additional - universes and constraints if any *) - defined - then - UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) - else uctx - in - update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto - | _ -> - CErrors.anomaly - Pp.( - str - "[obligation_terminator] close_proof returned more than one proof \ - term") - -(* Similar to the terminator but for the admitted path; this assumes - the admitted constant was already declared. - - FIXME: There is duplication of this code with obligation_terminator - and Obligations.admit_obligations *) -let obligation_admitted_terminator {name; num; auto} ctx' dref = - let prg = Option.get (State.find name) in - let {obls; remaining = rem} = prg.prg_obligations in - let obl = obls.(num) in - let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in - let transparent = evaluable_constant cst (Global.env ()) in - let () = - match obl.obl_status with - | true, Evar_kinds.Expand | true, Evar_kinds.Define true -> - if not transparent then err_not_transp () - | _ -> () - in - let inst, ctx' = - if not prg.prg_poly (* Not polymorphic *) then - (* The universe context was declared globally, we continue - from the new global environment. *) - let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in - let ctx' = UState.merge_subst ctx (UState.subst ctx') in - Univ.Instance.empty, ctx' - else - (* We get the right order somehow, but surely it could be enforced in a clearer way. *) - let uctx = UState.context ctx' in - Univ.UContext.instance uctx, ctx' - in - let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in - let () = if transparent then add_hint true prg cst in - update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli deleted file mode 100644 index 0e56475326..0000000000 --- a/vernac/declareObl.mli +++ /dev/null @@ -1,175 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr - -type 'a obligation_body = DefinedObl of 'a | TermObl of constr - -module Obligation : sig - - type t = private - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } - - val set_type : typ:Constr.types -> t -> t - val set_body : body:pconstant obligation_body -> t -> t - -end - -type obligations = - { obls : Obligation.t array - ; remaining : int } - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -(* Information about a single [Program {Definition,Lemma,..}] declaration *) -module ProgramDecl : sig - - type t = private - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : Declare.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : Declare.Hook.t option - ; prg_opaque : bool - } - - val make : - ?opaque:bool - -> ?hook:Declare.Hook.t - -> Names.Id.t - -> udecl:UState.universe_decl - -> uctx:UState.t - -> impargs:Impargs.manual_implicits - -> poly:bool - -> scope:Declare.locality - -> kind:Decls.definition_object_kind - -> Constr.constr option - -> Constr.types - -> Names.Id.t list - -> fixpoint_kind option - -> Vernacexpr.decl_notation list - -> RetrieveObl.obligation_info - -> (Constr.constr -> Constr.constr) - -> t - - val set_uctx : uctx:UState.t -> t -> t -end - -(** [declare_obligation] Save an obligation *) -val declare_obligation : - ProgramDecl.t - -> Obligation.t - -> Constr.types - -> Constr.types option - -> Entries.universes_entry - -> bool * Obligation.t - -module State : sig - - val num_pending : unit -> int - val first_pending : unit -> ProgramDecl.t option - - (** Returns [Error duplicate_list] if not a single program is open *) - val get_unique_open_prog : - Id.t option -> (ProgramDecl.t, Id.t list) result - - (** Add a new obligation *) - val add : Id.t -> ProgramDecl.t -> unit - - val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a - - val all : unit -> ProgramDecl.t list - - val find : Id.t -> ProgramDecl.t option - - (* Internal *) - type t - val prg_tag : t Summary.Dyn.tag -end - -val declare_definition : ProgramDecl.t -> Names.GlobRef.t - -(** Resolution status of a program *) -type progress = - | Remain of int - (** n obligations remaining *) - | Dependent - (** Dependent on other definitions *) - | Defined of GlobRef.t - (** Defined as id *) - -type obligation_resolver = - Id.t option - -> Int.Set.t - -> unit Proofview.tactic option - -> progress - -type obligation_qed_info = - { name : Id.t - ; num : int - ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress - } - -(** [obligation_terminator] part 2 of saving an obligation, proof mode *) -val obligation_terminator : - Evd.side_effects Declare.proof_entry list - -> UState.t - -> obligation_qed_info - -> unit - -(** [obligation_admitted_terminator] part 2 of saving an obligation, non-interactive mode *) -val obligation_admitted_terminator : - obligation_qed_info -> UState.t -> GlobRef.t -> unit - -(** [update_obls prg obls n progress] What does this do? *) -val update_obls : - ProgramDecl.t - -> Obligation.t array - -> int - -> progress - -(** Check obligations are properly solved before closing the - [what_for] section / module *) -val check_solved_obligations : what_for:Pp.t -> unit - -(** { 2 Util } *) - -val obl_substitution : - bool - -> Obligation.t array - -> Int.Set.t - -> (Id.t * (Constr.types * Constr.types)) list - -val dependencies : Obligation.t array -> int -> Int.Set.t -val err_not_transp : unit -> unit - -(* This is a hack to make it possible for Obligations to craft a Qed - * behind the scenes. The fix_exn the Stm attaches to the Future proof - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index c2e6ae9a5a..15c4b44581 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -25,7 +25,7 @@ module Proof_ending = struct type t = | Regular - | End_obligation of DeclareObl.obligation_qed_info + | End_obligation of Declare.Obls.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit @@ -291,7 +291,7 @@ let finish_admitted ~info ~uctx pe = (* If the constant was an obligation we need to update the program map *) match CEphemeron.get info.Info.proof_ending with | Proof_ending.End_obligation oinfo -> - DeclareObl.obligation_admitted_terminator oinfo uctx (List.hd cst) + Declare.Obls.obligation_admitted_terminator oinfo uctx (List.hd cst) | _ -> () let save_lemma_admitted ~(lemma : t) = @@ -383,7 +383,7 @@ let finalize_proof proof_obj proof_info = | Regular -> finish_proved proof_obj proof_info | End_obligation oinfo -> - DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo + Declare.Obls.obligation_terminator proof_obj.entries proof_obj.uctx oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~entries:proof_obj.entries | End_equations { hook; i; types; sigma } -> diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index b1462f1ce5..edc5f33e34 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -33,7 +33,7 @@ module Proof_ending : sig type t = | Regular - | End_obligation of DeclareObl.obligation_qed_info + | End_obligation of Declare.Obls.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit diff --git a/vernac/locality.ml b/vernac/locality.ml index f62eed5e41..3953e54f52 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -10,9 +10,12 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + let importability_of_bool = function - | true -> Declare.ImportNeedQualified - | false -> Declare.ImportDefaultBehavior + | true -> ImportNeedQualified + | false -> ImportDefaultBehavior (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -34,15 +37,14 @@ let warn_local_declaration = strbrk "available without qualification when imported.") let enforce_locality_exp locality_flag discharge = - let open Declare in let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) - | None, NoDischarge -> Global Declare.ImportDefaultBehavior + | None, NoDischarge -> Global ImportDefaultBehavior | None, DoDischarge when not (Global.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); - Global Declare.ImportNeedQualified + Global ImportNeedQualified | None, DoDischarge -> Discharge | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") diff --git a/vernac/locality.mli b/vernac/locality.mli index bf65579efd..81da895568 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -10,6 +10,9 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -20,7 +23,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a1ddd9f3b2..b84e20f6d0 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -14,9 +14,9 @@ open Pp open Util (* For the records fields, opens should go away one these types are private *) -open DeclareObl -open DeclareObl.Obligation -open DeclareObl.ProgramDecl +open Declare.Obls +open Declare.Obls.Obligation +open Declare.Obls.ProgramDecl let reduce c = let env = Global.env () in @@ -59,7 +59,7 @@ let default_tactic = ref (Proofview.tclUNIT ()) let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) let subst_deps expand obls deps t = - let osubst = DeclareObl.obl_substitution expand obls deps in + let osubst = Declare.Obls.obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let subst_deps_obl obls obl = @@ -141,7 +141,7 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in - let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in + let proof_ending = Lemmas.Proof_ending.End_obligation (Declare.Obls.{name = prg.prg_name; num; auto}) in let info = Lemmas.Info.make ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in @@ -314,7 +314,7 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) let {obls;_} = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose (msg_generating_obl name) obls; - let cst = DeclareObl.declare_definition prg in + let cst = Declare.Obls.declare_definition prg in Defined cst) else let () = Flags.if_verbose (msg_generating_obl name) obls in @@ -374,7 +374,7 @@ let admit_prog prg = obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; - DeclareObl.update_obls prg obls 0 + Declare.Obls.update_obls prg obls 0 (* get_any_prog *) let rec admit_all_obligations () = diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 0cd1ebf5dc..102a17b216 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -84,7 +84,7 @@ val add_definition : -> ?hook:Declare.Hook.t -> ?opaque:bool -> RetrieveObl.obligation_info - -> DeclareObl.progress + -> Declare.Obls.progress (* XXX: unify with MutualEntry *) @@ -102,7 +102,7 @@ val add_mutual_definitions : -> ?hook:Declare.Hook.t -> ?opaque:bool -> Vernacexpr.decl_notation list - -> DeclareObl.fixpoint_kind + -> Declare.Obls.fixpoint_kind -> unit (** Implementation of the [Obligation] command *) @@ -117,7 +117,7 @@ val next_obligation : (** Implementation of the [Solve Obligation] command *) val solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress + Names.Id.t option -> unit Proofview.tactic option -> Declare.Obls.progress val solve_all_obligations : unit Proofview.tactic option -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index a09a473afe..1cad052bce 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -16,7 +16,6 @@ Metasyntax DeclareUniv RetrieveObl Declare -DeclareObl ComHints Canonical RecLemmas diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 53a6409b22..106fed124e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1071,7 +1071,7 @@ let msg_of_subsection ss id = let vernac_end_segment ({v=id} as lid) = let ss = Lib.find_opening_node id in let what_for = msg_of_subsection ss lid.v in - DeclareObl.check_solved_obligations ~what_for; + Declare.Obls.check_solved_obligations ~what_for; match ss with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid |