diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 4 | ||||
| -rw-r--r-- | vernac/comFixpoint.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 55 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 21 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
6 files changed, 51 insertions, 44 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 37af8e1f55..bb5ebd7148 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -373,10 +373,10 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t the refinement manually.*) let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in - let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in + let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in let info = Lemmas.Info.make ~hook () in - let lemma = Lemmas.start_lemma ~name:id ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in + let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = if not (Option.is_empty term) then diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 31c2053148..6d9aa746b9 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -269,7 +269,7 @@ let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,f Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~kind:(local,poly,DefinitionBody fix_kind) ~udecl + Lemmas.start_lemma_with_initialization ~poly ~kind:(local,DefinitionBody fix_kind) ~udecl evd (Some(cofix,indexes,init_tac)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index c3dfdd1c0f..d323493c11 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -246,7 +246,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i +let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq i { Recthm.name; typ; impargs } = let t_i = norm typ in let k = IsAssumption Conjectural in @@ -261,7 +261,7 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i Univ.ContextSet.of_context univs | Monomorphic_entry univs -> univs in - let c = SectionLocalAssum ((t_i, univs),p,impl) in + let c = SectionLocalAssum ((t_i, univs),poly,impl) in let _ = declare_variable name (Lib.cwd(),c,k) in (VarRef name,impargs) | Global local -> @@ -338,19 +338,19 @@ module Stack = struct end (* Starting a goal *) -let start_lemma ~name ~kind +let start_lemma ~name ~poly ~kind ?(udecl=UState.default_univ_decl) ?(sign=initialize_named_context_for_proof()) ?(info=Info.make ()) sigma c = let goals = [ Global.env_of_context sign , c ] in - let proof = Proof_global.start_proof sigma name udecl kind goals in + let proof = Proof_global.start_proof sigma name udecl ~poly kind goals in { proof ; info } -let start_dependent_lemma ~name ~kind +let start_dependent_lemma ~name ~poly ~kind ?(udecl=UState.default_univ_decl) ?(info=Info.make ()) telescope = - let proof = Proof_global.start_dependent_proof name udecl kind telescope in + let proof = Proof_global.start_dependent_proof name udecl ~poly kind telescope in { proof; info } let rec_tac_initializer finite guard thms snl = @@ -367,7 +367,7 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl = +let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms snl = let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with | Some (finite,guard,init_tac) -> @@ -392,13 +392,13 @@ let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl = ; other_thms ; proof_ending = CEphemeron.create Proof_ending.Regular } in - let lemma = start_lemma ~name ~kind ~udecl ~info sigma typ in + let lemma = start_lemma ~name ~poly ~kind ~udecl ~info sigma typ in pf_map (Proof_global.map_proof (fun p -> match init_tac with | None -> p | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma -let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms = +let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in @@ -409,7 +409,7 @@ let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms = let hook = inference_hook in let evd = solve_remaining_evars ?hook flags env evd in let ids = List.map RelDecl.get_name ctx in - check_name_freshness (pi1 kind) id; + check_name_freshness (fst kind) id; (* XXX: The nf_evar is critical !! *) evd, (id.CAst.v, (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), @@ -424,14 +424,14 @@ let start_lemma_com ~program_mode ~kind ?inference_hook ?hook thms = let () = let open UState in if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd udecl) + ignore (Evd.check_univ_decl ~poly evd udecl) in let evd = - if pi2 kind then evd + if poly then evd else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_lemma_with_initialization ?hook ~kind evd ~udecl recguard thms snl + start_lemma_with_initialization ?hook ~poly ~kind evd ~udecl recguard thms snl (************************************************************************) (* Admitting a lemma-like constant *) @@ -449,19 +449,19 @@ let warn_let_as_axiom = (* This declares implicits and calls the hooks for all the theorems, including the main one *) -let process_recthms ?fix_exn ?hook env sigma ctx decl strength ref imps other_thms = +let process_recthms ?fix_exn ?hook env sigma ctx decl ~poly strength ref imps other_thms = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm ctx ref in let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly:(pi2 strength) ctx decl in - List.map_i (save_remaining_recthms env sigma strength norm uctx body opaq) 1 other_thms in + let uctx = UState.check_univ_decl ~poly ctx decl in + List.map_i (save_remaining_recthms env sigma ~poly strength norm uctx body opaq) 1 other_thms in let thms_data = (ref,imps)::other_thms_data in List.iter (fun (ref,imps) -> maybe_declare_manual_implicits false ref imps; - DeclareDef.Hook.call ?fix_exn ?hook ctx [] (pi1 strength) ref) thms_data + DeclareDef.Hook.call ?fix_exn ?hook ctx [] (fst strength) ref) thms_data let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref @@ -470,7 +470,7 @@ let get_keep_admitted_vars = ~key:["Keep"; "Admitted"; "Variables"] ~value:true -let finish_admitted env sigma id (scope,poly,kind) pe ctx hook udecl impargs other_thms = +let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs other_thms = let local = match scope with | Global local -> local | Discharge -> warn_let_as_axiom id; ImportNeedQualified @@ -479,7 +479,7 @@ let finish_admitted env sigma id (scope,poly,kind) pe ctx hook udecl impargs oth let () = assumption_message id in Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx udecl (Global local,poly,kind) (ConstRef kn) impargs other_thms; + process_recthms ?fix_exn:None ?hook env sigma ctx udecl ~poly (Global local,kind) (ConstRef kn) impargs other_thms; Feedback.feedback Feedback.AddedAxiom let save_lemma_admitted ?proof ~(lemma : t) = @@ -489,14 +489,17 @@ let save_lemma_admitted ?proof ~(lemma : t) = | Some ({ id; entries; persistence = k; universes; udecl }, { Info.hook; impargs; other_thms; _} ) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { proof_entry_secctx; proof_entry_type } = List.hd entries in + let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in if proof_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); + let poly = match proof_entry_universes with + | Entries.Monomorphic_entry _ -> false + | Entries.Polymorphic_entry (_, _) -> true in let typ = Option.get proof_entry_type in - let ctx = UState.univ_entry ~poly:(pi2 k) universes in + let ctx = UState.univ_entry ~poly universes in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in let sigma = Evd.from_env env in - finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms + finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms | None -> let pftree = Proof_global.get_proof lemma.proof in let gk = Proof_global.get_persistence lemma.proof in @@ -526,7 +529,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let { Info.hook; impargs; other_thms } = lemma.info in let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook udecl impargs other_thms + finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms (************************************************************************) (* Saving a lemma-like constant *) @@ -536,7 +539,7 @@ let finish_proved env sigma opaque idopt po info = let open Proof_global in let { Info.hook; compute_guard; impargs; other_thms } = info in match po with - | { id; entries=[const]; persistence=locality,poly,kind; universes; udecl } -> + | { id; entries=[const]; persistence=locality,kind; universes; udecl; poly } -> let is_opaque = match opaque with | Transparent -> false | Opaque -> true @@ -570,7 +573,7 @@ let finish_proved env sigma opaque idopt po info = in definition_message id; (* This takes care of the implicits and hook for the current constant*) - process_recthms ~fix_exn ?hook env sigma universes udecl (locality,poly,kind) r impargs other_thms + process_recthms ~fix_exn ?hook env sigma universes udecl ~poly (locality,kind) r impargs other_thms with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -627,7 +630,7 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = let open Decl_kinds in let obls = ref 1 in - let kind = match pi3 proof_obj.Proof_global.persistence with + let kind = match snd proof_obj.Proof_global.persistence with | DefinitionBody d -> IsDefinition d | Proof p -> IsProof p in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 28b9c38072..1a8b1f2f30 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -93,6 +93,7 @@ end (** Starts the proof of a constant *) val start_lemma : name:Id.t + -> poly:bool -> kind:goal_kind -> ?udecl:UState.universe_decl -> ?sign:Environ.named_context_val @@ -103,6 +104,7 @@ val start_lemma val start_dependent_lemma : name:Id.t + -> poly:bool -> kind:goal_kind -> ?udecl:UState.universe_decl -> ?info:Info.t @@ -114,6 +116,7 @@ type lemma_possible_guards = int list list (** Pretty much internal, only used in ComFixpoint *) val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t + -> poly:bool -> kind:goal_kind -> udecl:UState.universe_decl -> Evd.evar_map @@ -127,6 +130,7 @@ val default_thm_id : Names.Id.t (** Main [Lemma foo args : type.] command *) val start_lemma_com : program_mode:bool + -> poly:bool -> kind:goal_kind -> ?inference_hook:Pretyping.inference_hook -> ?hook:DeclareDef.Hook.t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4e4f80fd71..b2c5520c0b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -388,16 +388,14 @@ let deps_remaining obls deps = deps [] -let goal_kind poly = - Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition) +let goal_kind = Decl_kinds.(Global ImportNeedQualified, DefinitionBody Definition) +let goal_proof_kind = Decl_kinds.(Global ImportNeedQualified, Proof Lemma) -let goal_proof_kind poly = - Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma) - -let kind_of_obligation poly o = +let kind_of_obligation o = match o with - | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly - | _ -> goal_proof_kind poly + | Evar_kinds.Define false + | Evar_kinds.Expand -> goal_kind + | _ -> goal_proof_kind let rec string_of_list sep f = function [] -> "" @@ -415,7 +413,7 @@ let solve_by_tac ?loc name evi t poly ctx = try let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in + id ~poly ~goal_kind ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in let (body, eff) = Future.force entry.Proof_global.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in @@ -486,14 +484,15 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in + let kind = kind_of_obligation (snd obl.obl_status) in 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 hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in let info = Lemmas.Info.make ~hook ~proof_ending () in - let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~kind ~info evd (EConstr.of_constr obl.obl_type) in + let poly = pi2 prg.prg_kind in + let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~kind ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in lemma diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index da8808ccaa..d1377fecc5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -560,7 +560,7 @@ let () = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ?hook k l = +let start_proof_and_print ~program_mode ~poly ?hook k l = let inference_hook = if program_mode then let hook env sigma ev = @@ -582,7 +582,7 @@ let start_proof_and_print ~program_mode ?hook k l = in Some hook else None in - start_lemma_com ~program_mode ?inference_hook ?hook ~kind:k l + start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~kind:k l let vernac_definition_hook p = function | Coercion -> @@ -614,8 +614,9 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in let program_mode = atts.program in + let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)] + start_proof_and_print ~program_mode ~poly (local, DefinitionBody kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -638,7 +639,7 @@ let vernac_start_proof ~atts kind l = let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l + start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic (local, Proof kind) l let vernac_end_proof ?stack ?proof = let open Vernacexpr in function | Admitted -> |