diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comFixpoint.ml | 55 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 53 | ||||
| -rw-r--r-- | vernac/declareDef.mli | 29 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 86 | ||||
| -rw-r--r-- | vernac/declareObl.mli | 3 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 58 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 15 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.ml | 23 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 5 |
11 files changed, 174 insertions, 161 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0a70954dd2..6580495295 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -236,16 +236,22 @@ let interp_fixpoint ~cofix l = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = - let fix_kind, cofix, indexes = match indexes with - | Some indexes -> Decls.Fixpoint, false, indexes - | None -> Decls.CoFixpoint, true, [] +let build_recthms ~indexes fixnames fixtypes fiximps = + let fix_kind, cofix = match indexes with + | Some indexes -> Decls.Fixpoint, false + | None -> Decls.CoFixpoint, true in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { Lemmas.Recthm.name; typ + { DeclareDef.Recthm.name; typ ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) - fixnames fixtypes fiximps in + fixnames fixtypes fiximps + in + fix_kind, cofix, thms + +let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = + let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in + let indexes = Option.default [] indexes in let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = @@ -255,40 +261,17 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let indexes, cofix, fix_kind = - match indexes with - | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint) - | None -> [], true, Decls.(IsDefinition CoFixpoint) - in +let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = (* We shortcut the proof process *) + let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, gidx = - if not cofix then - let env = Global.env() in - let indexes = Pretyping.search_guard env indexes fixdecls in - let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in - let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in - vars, fixdecls, Some indexes - else (* cofix *) - let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - vars, fixdecls, None - in - let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let ubind = Evd.universe_binders evd in + let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let fix_kind = Decls.IsDefinition fix_kind in let _ : GlobRef.t list = - List.map4 (fun name body types impargs -> - let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in - DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce) - fixnames fixdecls fixtypes fiximps + DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx + ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + fixitems in - Declare.recursive_message (not cofix) gidx fixnames; - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () let extract_decreasing_argument ~structonly { CAst.v = v; _ } = diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 09582f4ef2..fc53abdcea 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,6 +69,59 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref +let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = + match possible_indexes with + | Some possible_indexes -> + let env = Global.env() in + let indexes = Pretyping.search_guard env possible_indexes rec_declaration in + let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in + let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in + vars, fixdecls, Some indexes + | None -> + let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + vars, fixdecls, None + +module Recthm = struct + type t = + { name : Names.Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Names.Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = + let vars, fixdecls, indexes = + mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in + let ubind, univs = + (* XXX: Obligations don't do this, this seems like a bug? *) + if restrict_ucontext + then + let evd = Evd.from_ctx uctx in + let evd = Evd.restrict_universe_context evd vars in + let univs = Evd.check_univ_decl ~poly evd udecl in + Evd.universe_binders evd, univs + else + let univs = UState.univ_entry ~poly uctx in + UnivNames.empty_binders, univs + in + let csts = CList.map2 + (fun Recthm.{ name; typ; impargs } body -> + let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in + declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + fixitems fixdecls + in + let isfix = Option.is_empty possible_indexes in + let fixnames = List.map (fun { Recthm.name } -> name) fixitems in + Declare.recursive_message isfix indexes fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; + csts + let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index fb1fc9242c..1d7fd3a3bf 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -59,6 +59,35 @@ val declare_assumption -> Entries.parameter_entry -> GlobRef.t +module Recthm : sig + type t = + { name : Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +val declare_mutually_recursive + : opaque:bool + -> scope:locality + -> kind:Decls.logical_kind + -> poly:bool + -> uctx:UState.t + -> udecl:UState.universe_decl + -> ntns:Vernacexpr.decl_notation list + -> rec_declaration:Constr.rec_declaration + -> possible_indexes:int list list option + -> ?restrict_ucontext:bool + (** XXX: restrict_ucontext should be always true, this seems like a + bug in obligations, so this parameter should go away *) + -> Recthm.t list + -> Names.GlobRef.t list + val prepare_definition : allow_evars:bool -> ?opaque:bool diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 626dcd5d34..98a9e4b9c9 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -251,43 +251,22 @@ let get_prg_info_map () = !from_prg let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] -let close sec = +let check_can_close sec = if not (ProgMap.is_empty !from_prg) then let keys = map_keys !from_prg in CErrors.user_err ~hdr:"Program" Pp.( str "Unsolved obligations when closing " - ++ str sec ++ str ":" ++ spc () + ++ Id.print sec ++ str ":" ++ spc () ++ prlist_with_sep spc (fun x -> Id.print x) keys ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ str "unsolved obligations" )) -let input : ProgramDecl.t CEphemeron.key ProgMap.t -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi) - ; load_function = (fun _ (_, pi) -> from_prg := pi) - ; discharge_function = - (fun _ -> - close "section"; - None ) - ; classify_function = - (fun _ -> - close "module"; - Dispose ) } - -let map_replace k v m = - ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) - -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) - -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) +let prgmap_op f = from_prg := f !from_prg +let progmap_remove prg = prgmap_op (ProgMap.remove prg.prg_name) +let progmap_add n prg = prgmap_op (ProgMap.add n prg) +let progmap_replace prg = prgmap_op (map_replace prg.prg_name prg) let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 @@ -457,48 +436,35 @@ let declare_mutual_definition l = (xdef :: defs, xobls @ obls)) l ([], []) in (* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs 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, + DeclareDef.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 fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let fixnames = first.prg_deps in - let opaque = first.prg_opaque in - let indexes, fixdecls = + let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in + let possible_indexes = match fixkind with | IsFixpoint wfl -> - let possible_indexes = - List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes - in - let indexes = - Pretyping.search_guard (Global.env ()) possible_indexes fixdecls - in - ( Some indexes - , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l - ) - | IsCoFixpoint -> - (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l) + 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 poly = first.prg_poly in - let scope = first.prg_scope in - let univs = UState.univ_entry ~poly first.prg_ctx in - let fix_exn = Hook.get get_fix_exn () in - let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in - let ubind = UnivNames.empty_binders in + let udecl = UState.default_univ_decl in let kns = - List.map4 - (fun name body types impargs -> - let ce = Declare.definition_entry ~opaque ~types ~univs body in - DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce) - fixnames fixdecls fixtypes fiximps + DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind + ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly + ~restrict_ucontext:false fixitems in - (* Declare notations *) - List.iter - (Metasyntax.add_notation_interpretation (Global.env ())) - first.prg_notations; - Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; + (* Only for the first constant *) + let fix_exn = Hook.get get_fix_exn () in let dref = List.hd kns in DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 4e20c7c192..16c0413caf 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -139,6 +139,9 @@ val update_obls : (** { 2 Util } *) +(** Check obligations are properly solved before closing a section *) +val check_can_close : Id.t -> unit + val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t val program_tcc_summary_tag : diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 1d790e7cd2..5dae389a62 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -368,7 +368,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl)) | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) -| TTBigint -> MayRecNo (Aentry Prim.bigint) +| TTBigint -> MayRecNo (Aentry Prim.bignat) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with @@ -411,8 +411,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v))) end | TTReference -> begin match forpat with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7782ff8ac9..e08d2ce117 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -39,15 +39,6 @@ module Proof_ending = struct end -module Recthm = struct - type t = - { name : Id.t - ; typ : Constr.t - ; args : Name.t list - ; impargs : Impargs.manual_implicits - } -end - module Info = struct type t = @@ -56,7 +47,7 @@ module Info = struct ; impargs : Impargs.manual_implicits ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; other_thms : Recthm.t list + ; other_thms : DeclareDef.Recthm.t list ; scope : DeclareDef.locality ; kind : Decls.logical_kind } @@ -129,7 +120,7 @@ let start_dependent_lemma ~name ~poly let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with + match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -137,12 +128,12 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with + in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = - let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in + let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with | Some (finite,guard,init_terms) -> let rec_tac = rec_tac_initializer finite guard thms snl in @@ -162,7 +153,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua intro_tac (List.hd thms), [] in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { Recthm.name; typ; impargs; _}::other_thms -> + | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms -> let info = Info.{ hook ; impargs @@ -185,25 +176,25 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua (* XXX: Most of this does belong to Declare, due to proof_entry manip *) module MutualEntry : sig - (* We keep this type abstract and to avoid uncontrolled hacks *) - type t - - val variable : info:Info.t -> Entries.parameter_entry -> t - - val adjust_guardness_conditions + val declare_variable : info:Info.t - -> Evd.side_effects Declare.proof_entry - -> t + -> uctx:UState.t + (* Only for the first constant, introduced by compat *) + -> ubind:UnivNames.universe_binders + -> name:Id.t + -> Entries.parameter_entry + -> Names.GlobRef.t list val declare_mutdef (* Common to all recthms *) - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + : info:Info.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> uctx:UState.t -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list (* Only for the first constant, introduced by compat *) -> ubind:UnivNames.universe_binders -> name:Id.t - -> t + -> Evd.side_effects Declare.proof_entry -> Names.GlobRef.t list end = struct @@ -219,8 +210,6 @@ end = struct ; info : Info.t } - let variable ~info t = { entry = NoBody t; info } - (* XXX: Refactor this with the code in [ComFixpoint.declare_fixpoint_generic] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = @@ -290,9 +279,17 @@ end = struct let ubind = UnivNames.empty_binders in let rs = List.map_i ( - fun i { Recthm.name; typ; impargs } -> + fun i { DeclareDef.Recthm.name; typ; impargs } -> declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms in r :: rs + + let declare_variable ~info ~uctx ~ubind ~name pe = + declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info } + + let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const = + let mutpe = adjust_guardness_conditions ~info const in + declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe + end (************************************************************************) @@ -320,10 +317,8 @@ let compute_proof_using_for_admitted proof typ pproofs = | _ -> None let finish_admitted ~name ~info ~uctx pe = - let mutpe = MutualEntry.variable ~info pe in let ubind = UnivNames.empty_binders in - let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~uctx ~ubind ~name mutpe in + let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in () let save_lemma_admitted ~(lemma : t) : unit = @@ -361,11 +356,10 @@ let finish_proved idopt po info = | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in let fix_exn = Declare.Internal.get_fix_exn const in let () = try - let mutpe = MutualEntry.adjust_guardness_conditions ~info const in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in let ubind = UState.universe_binders uctx in let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~fix_exn ~uctx ?hook_data ~ubind ~name mutpe + MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const in () with e when CErrors.noncritical e -> let e = Exninfo.capture e in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 471c955311..6a1f8c09f3 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -44,19 +44,6 @@ module Proof_ending : sig end -module Recthm : sig - type t = - { name : Id.t - (** Name of theorem *) - ; typ : Constr.t - (** Type of theorem *) - ; args : Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - module Info : sig type t @@ -104,7 +91,7 @@ val start_lemma_with_initialization -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * Constr.t option list option) option - -> Recthm.t list + -> DeclareDef.Recthm.t list -> int list option -> t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 22e4e35ad4..475d5c31f7 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -252,7 +252,7 @@ let quote_notation_token x = let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> - NumTok.of_string x <> None + NumTok.Unsigned.parse_string x <> None | _ -> false diff --git a/vernac/obligations.ml b/vernac/obligations.ml index f449cb02f1..a29ba44907 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -17,11 +17,8 @@ open Printf - Apply term prefixed by quantification on "existentials". *) -open Term open Constr -open Vars open Names -open Evd open Pp open CErrors open Util @@ -41,7 +38,7 @@ let check_evars env evm = (fun key evi -> if Evd.is_obligation_evar evm key then () else - let (loc,k) = evar_source key evm in + let (loc,k) = Evd.evar_source key evm in Pretype_errors.error_unsolvable_implicit ?loc env evm key None) (Evd.undefined_map evm) @@ -133,14 +130,14 @@ let etype_of_evar evm evs hyps concl = | LocalDef (id,c,_) -> let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, + Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, Int.Set.union s'' s', Id.Set.union trans'' trans' | LocalAssum (id,_) -> - mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') + Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') | [] -> - let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in - subst_vars acc 0 t', s, trans + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in + subst_vars acc 0 t', s, trans in aux [] 0 (List.rev hyps) let trunc_named_context n ctx = @@ -152,14 +149,14 @@ let rec chop_product n t = if Int.equal n 0 then Some t else match Constr.kind t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None + | Prod (_, _, b) -> if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None let evar_dependencies evm oev = let one_step deps = Evar.Set.fold (fun ev s -> let evi = Evd.find evm ev in - let deps' = evars_of_filtered_evar_info evm evi in + let deps' = Evd.evars_of_filtered_evar_info evm evi in if Evar.Set.mem oev deps' then invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) else Evar.Set.union deps' s) @@ -215,13 +212,13 @@ let eterm_obligations env name evm fs ?status t ty = (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs | None -> evtyp, hyps, 0 in - let loc, k = evar_source id evm in + let loc, k = Evd.evar_source id evm in let status = match k with | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o | _ -> match status with @@ -282,7 +279,7 @@ let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) -let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) +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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8a4522296f..8641c67d9f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -501,7 +501,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in + { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in let () = let open UState in if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then @@ -983,7 +983,7 @@ let vernac_begin_section ~poly ({v=id} as lid) = to its current value ie noop. *) set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly -let vernac_end_section {CAst.loc} = +let vernac_end_section {CAst.loc; v} = Dumpglob.dump_reference ?loc (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section () @@ -993,6 +993,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) let vernac_end_segment ({v=id} as lid) = + DeclareObl.check_can_close lid.v; match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid |