diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 9 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 29 | ||||
| -rw-r--r-- | toplevel/command.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
5 files changed, 31 insertions, 15 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index ec2c95048..627633ad5 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -493,13 +493,15 @@ let new_instance ctx (instid, bk, cl) props = in let kn = Declare.declare_constant id cdecl in Flags.if_verbose Command.definition_message id; - hook kn + hook kn; + Some id else let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false); Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) (!refine_ref (evm, term)); - Flags.if_verbose (msg $$ Printer.pr_open_subgoals) () + Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); + None @@ -529,7 +531,8 @@ let context l = let sigma = Evd.evars_of !isevars in let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in List.iter (function (id,_,t) -> - Command.declare_one_assumption false (Local (* global *), Definitional) t false (* inline *) (dummy_loc, id)) + Command.declare_one_assumption false (Local (* global *), Definitional) t + [] false (* inline *) (dummy_loc, id)) (List.rev fullctx) open Libobject diff --git a/toplevel/classes.mli b/toplevel/classes.mli index f305fc805..809888f0d 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -43,7 +43,7 @@ val new_instance : local_binder list -> typeclass_constraint -> binder_def_list -> - unit + identifier option val context : typeclass_context -> unit diff --git a/toplevel/command.ml b/toplevel/command.ml index ccdb906ce..ffe4c26d5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -177,7 +177,7 @@ let syntax_definition ident c local onlyparse = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c nl (_,ident) = +let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = @@ -191,11 +191,14 @@ let declare_one_assumption is_coe (local,kind) c nl (_,ident) = | (Global|Local) -> let kn = declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in + let gr = ConstRef kn in + if Impargs.is_implicit_args () || imps <> [] then + declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps; assumption_message ident; if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); - ConstRef kn in + gr in if is_coe then Class.try_add_new_coercion r local let declare_assumption_hook = ref ignore @@ -204,9 +207,12 @@ let set_declare_assumption_hook = (:=) declare_assumption_hook let declare_assumption idl is_coe k bl c nl= if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in - let c = interp_type Evd.empty (Global.env()) c in - !declare_assumption_hook c; - List.iter (declare_one_assumption is_coe k c nl) idl + let sigma = Evd.empty and env = Global.env () in + let ic = intern_type sigma env c in + let imps = Implicit_quantifiers.implicits_of_rawterm ic in + let j = Default.understand_judgment sigma env ic in + !declare_assumption_hook j.uj_val; + List.iter (declare_one_assumption is_coe k j.uj_val imps nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -1026,9 +1032,16 @@ let start_proof_com sopt kind (bl,t) hook = (Pfedit.get_all_proof_names ()) in let env = Global.env () in - let c = interp_type Evd.empty env (generalize_constr_expr t bl) in - let _ = Typeops.infer_type env c in - start_proof id kind c hook + let sigma = Evd.empty in + let b = generalize_constr_expr t bl in + let ib = intern_type sigma env b in + let imps = Implicit_quantifiers.implicits_of_rawterm ib in + let j = Default.understand_judgment sigma env ib in + start_proof id kind j.uj_val + (fun str cst -> + if Impargs.is_implicit_args () || imps <> [] then + declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps; + hook str cst) let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then diff --git a/toplevel/command.mli b/toplevel/command.mli index 2dbc29538..d67daa83a 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -40,8 +40,8 @@ val declare_definition : identifier -> definition_kind -> val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit -val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool - -> Names.variable located -> unit +val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> + Impargs.manual_explicitation list -> bool -> Names.variable located -> unit val set_declare_assumption_hook : (types -> unit) -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 13b2bab5c..770cc5ccf 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -534,7 +534,7 @@ let vernac_class id par ar sup props = Classes.new_class id par ar sup props let vernac_instance sup inst props = - Classes.new_instance sup inst props + ignore(Classes.new_instance sup inst props) let vernac_context l = Classes.context l |