diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 58 |
1 files changed, 26 insertions, 32 deletions
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 |