diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 88 | ||||
| -rw-r--r-- | vernac/classes.mli | 3 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 5 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 21 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 10 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 31 |
7 files changed, 87 insertions, 73 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index e9a0ed7c34..0333b73ffe 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -401,7 +401,7 @@ let do_instance_subst_constructor_and_ty subst k u ctx = let term = it_mkLambda_or_LetIn (Option.get app) ctx in term, termtype -let do_instance_resolve_TC term termtype sigma env = +let do_instance_resolve_TC termtype sigma env = let sigma = Evarutil.nf_evar_map sigma in let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in (* Try resolving fields that are typeclasses automatically. *) @@ -447,15 +447,37 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = (push_rel_context ctx' env') sigma kcl_props props subst in res, sigma -let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id = - let term, termtype = - if List.is_empty k.cl_props then +let interp_props ~program_mode env' cty k u ctx ctx' subst sigma = function + | (true, { CAst.v = CRecord fs; loc }) -> + check_duplicate ?loc fs; + let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + term, termtype, sigma + | (_, term) -> + let sigma, def = + interp_casted_constr_evars ~program_mode env' sigma term cty in + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + term, termtype, sigma + +let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = + let term, termtype, sigma = match opt_props with + | Some props -> + on_pi1 (fun x -> Some x) + (interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props) + | None -> let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - Some term, termtype - else - None, it_mkProd_or_LetIn cty ctx in - let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + if List.is_empty k.cl_props then + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype + else + None, it_mkProd_or_LetIn cty ctx + in + let termtype, sigma = do_instance_resolve_TC termtype sigma env in + term, termtype, sigma + in Flags.silently (fun () -> declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl (List.map RelDecl.get_name ctx) term termtype) @@ -463,20 +485,9 @@ let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props = let term, termtype, sigma = - match props with - | (true, { CAst.v = CRecord fs; loc }) -> - check_duplicate ?loc fs; - let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - term, termtype, sigma - | (_, term) -> - let sigma, def = - interp_casted_constr_evars ~program_mode:false env' sigma term cty in - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - term, termtype, sigma in - let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in + interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props + in + let termtype, sigma = do_instance_resolve_TC termtype sigma env in if Evd.has_undefined sigma then CErrors.user_err Pp.(str "Unsolved obligations remaining.") else @@ -485,26 +496,15 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = let term, termtype, sigma = match opt_props with - | Some (true, { CAst.v = CRecord fs; loc }) -> - check_duplicate ?loc fs; - let subst, sigma = - do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - term, termtype, sigma - | Some (_, term) -> - let sigma, def = - interp_casted_constr_evars ~program_mode:true env' sigma term cty in - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - term, termtype, sigma + | Some props -> + interp_props ~program_mode:true env' cty k u ctx ctx' subst sigma props | None -> let subst, sigma = do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in let term, termtype = do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in term, termtype, sigma in - let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + let termtype, sigma = do_instance_resolve_TC termtype sigma env in if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then declare_instance_constant pri global imps ?hook id decl poly sigma term termtype else @@ -555,12 +555,13 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl = let new_instance_interactive ?(global=false) ~poly instid ctx cl - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook + pri opt_props = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:false ~generalize env instid ctx cl in - id, do_instance_interactive env sigma ?hook ~tac ~global ~poly - cty k u ctx ctx' pri decl imps subst id + id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly + cty k u ctx ctx' pri decl imps subst id opt_props let new_instance_program ?(global=false) ~poly instid ctx cl opt_props @@ -589,3 +590,10 @@ let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri = interp_instance_context ~program_mode ~generalize:false env ctx pl cl in do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid + +let refine_att = + let open Attributes in + let open Notations in + attribute_of_list ["refine",single_key_parser ~name:"refine" ~key:"refine" ()] >>= function + | None -> return false + | Some () -> return true diff --git a/vernac/classes.mli b/vernac/classes.mli index 1247fdc8c1..594df52c70 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -35,6 +35,7 @@ val new_instance_interactive -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr + -> (bool * constr_expr) option -> Id.t * Lemmas.t val new_instance @@ -84,3 +85,5 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u (** For generation on names based on classes only *) val id_of_class : typeclass -> Id.t + +val refine_att : bool Attributes.attribute diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 36aa7a37a2..80fcb7bc45 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -12,7 +12,6 @@ open Pp open CErrors open Sorts open Util -open Constr open Context open Environ open Names @@ -164,9 +163,7 @@ let sign_level env evd sign = match d with | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> - let s = destSort (Reduction.whd_all env - (EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))) - in + let s = Retyping.get_sort_of env evd (EConstr.of_constr (RelDecl.get_type d)) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) sign (Univ.Universe.sprop,env)) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 65cd4cd6a4..54dda09e83 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -972,6 +972,8 @@ let declare_modtype id args mtys mty_l = protect_summaries declare_mt let declare_include me_asts = + if Global.sections_are_opened () then + user_err Pp.(str "Include is not allowed inside sections."); protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index b4c0a33585..a78f4645c2 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -51,6 +51,7 @@ let decl_notation = Entry.create "vernac:decl_notation" let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" let section_subset_expr = Entry.create "vernac:section_subset_expr" +let scope_delimiter = Entry.create "vernac:scope_delimiter" let make_bullet s = let open Proof_bullet in @@ -65,8 +66,7 @@ let parse_compat_version = let open Flags in function | "8.11" -> Current | "8.10" -> V8_10 | "8.9" -> V8_9 - | "8.8" -> V8_8 - | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") | s -> @@ -718,7 +718,7 @@ END (* Extensions: implicits, coercions, etc. *) GRAMMAR EXTEND Gram - GLOBAL: gallina_ext hint_info; + GLOBAL: gallina_ext hint_info scope_delimiter; gallina_ext: [ [ (* Transparent and Opaque *) @@ -836,11 +836,11 @@ GRAMMAR EXTEND Gram { [`ClearImplicits; `ClearScopes] } ] ] ; - scope: + scope_delimiter: [ [ "%"; key = IDENT -> { key } ] ] ; argument_spec: [ - [ b = OPT "!"; id = name ; s = OPT scope -> + [ b = OPT "!"; id = name ; s = OPT scope_delimiter -> { id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc x) s } ] ]; @@ -853,7 +853,7 @@ GRAMMAR EXTEND Gram implicit_status = NotImplicit}] } | "/" -> { [`Slash] } | "&" -> { [`Ampersand] } - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in @@ -861,7 +861,7 @@ GRAMMAR EXTEND Gram `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = NotImplicit}) items } - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in @@ -869,7 +869,7 @@ GRAMMAR EXTEND Gram `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = Implicit}) items } - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in @@ -1137,11 +1137,8 @@ GRAMMAR EXTEND Gram positive_search_mark: [ [ "-" -> { false } | -> { true } ] ] ; - scope: - [ [ "%"; key = IDENT -> { key } ] ] - ; searchabout_query: - [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> + [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter -> { (b, SearchString (s,sc)) } | b = positive_search_mark; p = constr_pattern -> { (b, SearchSubPattern p) } diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cf322c52d0..865eded545 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -295,16 +295,18 @@ let save_lemma_admitted ~(lemma : t) : unit = | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") in let typ = EConstr.Unsafe.to_constr typ in - (* This will warn if the proof is complete *) - let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in + let proof = Proof_global.get_proof lemma.proof in + let pproofs = Proof.partial_proof proof in let sec_vars = if not (get_keep_admitted_vars ()) then None else match Proof_global.get_used_variables lemma.proof, pproofs with | Some _ as x, _ -> x - | None, (pproof, _) :: _ -> + | None, pproof :: _ -> let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in - let ids_def = Environ.global_vars_set env pproof in + (* [pproof] is evar-normalized by [partial_proof]. We don't + count variables appearing only in the type of evars. *) + let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None in let universes = Proof_global.get_initial_euctx lemma.proof in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6dfba02ae9..128c30908b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1048,27 +1048,27 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance_program ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in () -let vernac_instance_interactive ~atts name bl t info = +let vernac_instance_interactive ~atts name bl t info props = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id, pstate = - Classes.new_instance_interactive ~global ~poly name bl t info in + Classes.new_instance_interactive ~global ~poly name bl t info props in pstate let vernac_instance ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = @@ -2094,16 +2094,21 @@ let translate_vernac ~atts v = let open Vernacextend in match v with (* Type classes *) | VernacInstance (name, bl, t, props, info) -> - let { DefAttributes.program } = DefAttributes.parse atts in + let atts, program = Attributes.(parse_with_extra program) atts in if program then VtDefault (fun () -> vernac_instance_program ~atts name bl t props info) else begin match props with | None -> - VtOpenProof(fun () -> - vernac_instance_interactive ~atts name bl t info) + VtOpenProof (fun () -> + vernac_instance_interactive ~atts name bl t info None) | Some props -> - VtDefault(fun () -> - vernac_instance ~atts name bl t props info) + let atts, refine = Attributes.parse_with_extra Classes.refine_att atts in + if refine then + VtOpenProof (fun () -> + vernac_instance_interactive ~atts name bl t info (Some props)) + else + VtDefault (fun () -> + vernac_instance ~atts name bl t props info) end | VernacDeclareInstance (id, bl, inst, info) -> |