diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/command.ml | 19 | ||||
-rw-r--r-- | toplevel/command.mli | 6 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 26 |
3 files changed, 27 insertions, 24 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index aa9545210..eef22b8a2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -49,12 +49,16 @@ let red_constant_entry ce = function const_entry_type = ce.const_entry_type } -let definition_body_red ident n com comtypeopt red_option = +let definition_body_red red_option ident (local,n) com comtypeopt = + let warning () = + mSGERRNL [< 'sTR"Warning: "; pr_id ident; + 'sTR" is declared as a global definition" >] in let ce = constant_entry_of_com (com,comtypeopt) in let ce' = red_constant_entry ce red_option in match n with | NeverDischarge -> declare_constant ident (ConstantEntry ce',n); + if local then warning (); if is_verbose() then message ((string_of_id ident) ^ " is defined") | DischargeAt disch_sp -> if Lib.is_section_p disch_sp then begin @@ -67,13 +71,12 @@ let definition_body_red ident n com comtypeopt red_option = mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; 'sTR" is not visible from current goals" >] end else begin - mSGERRNL [< 'sTR"Warning: "; pr_id ident; - 'sTR" is declared as a global definition">]; declare_constant ident (ConstantEntry ce',n); + warning (); if is_verbose() then message ((string_of_id ident) ^ " is defined") end -let definition_body ident n com typ = definition_body_red ident n com typ None +let definition_body = definition_body_red None let syntax_definition ident com = let c = interp_rawconstr Evd.empty (Global.env()) com in @@ -96,8 +99,8 @@ let hypothesis_def_var is_refining ident n c = in match n with | NeverDischarge -> - warning(); - parameter_def_var ident c + parameter_def_var ident c; + warning() | DischargeAt disch_sp -> if Lib.is_section_p disch_sp then begin let t = interp_type Evd.empty (Global.env()) c in @@ -108,8 +111,8 @@ let hypothesis_def_var is_refining ident n c = mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 'sTR" is not visible from current goals" >] end else begin - warning(); - parameter_def_var ident c + parameter_def_var ident c; + warning() end (* 3| Mutual Inductive definitions *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 263d67032..8c34a3eb1 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -10,11 +10,11 @@ open Declare (* Declaration functions. The following functions take ASTs, transform them into [constr] and then call the corresponding functions of [Declare]. *) -val definition_body : identifier -> strength -> +val definition_body : identifier -> bool * strength -> Coqast.t -> Coqast.t option -> unit -val definition_body_red : identifier -> strength -> - Coqast.t -> Coqast.t option -> Tacred.red_expr option -> unit +val definition_body_red : Tacred.red_expr option -> + identifier -> bool * strength -> Coqast.t -> Coqast.t option -> unit val syntax_definition : identifier -> Coqast.t -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0a7aa7862..e94b73f18 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -776,22 +776,22 @@ let _ = Some t, Some redexp | _ -> bad_vernac_args "DEFINITION" in - let stre,coe,objdef,idcoe = match kind with - | "DEFINITION" -> NeverDischarge,false,false,false - | "COERCION" -> NeverDischarge,true,false,false - | "LCOERCION" -> make_strength_0(),true,false,false - | "LET" -> make_strength_2(),false,false,false - | "LOCAL" -> make_strength_0(),false,false,false - | "OBJECT" -> NeverDischarge,false,true,false - | "LOBJECT" -> make_strength_0(),false,true,false - | "OBJCOERCION" -> NeverDischarge,true,true,false - | "LOBJCOERCION" -> make_strength_0(),true,true,false - | "SUBCLASS" -> NeverDischarge,false,false,true - | "LSUBCLASS" -> make_strength_0(),false,false,true + let local,stre,coe,objdef,idcoe = match kind with + | "DEFINITION" -> false,NeverDischarge,false,false,false + | "COERCION" -> false,NeverDischarge,true,false,false + | "LCOERCION" -> true,make_strength_0(),true,false,false + | "LET" -> true,make_strength_2(),false,false,false + | "LOCAL" -> true,make_strength_0(),false,false,false + | "OBJECT" -> false,NeverDischarge,false,true,false + | "LOBJECT" -> true,make_strength_0(),false,true,false + | "OBJCOERCION" -> false,NeverDischarge,true,true,false + | "LOBJCOERCION" -> true,make_strength_0(),true,true,false + | "SUBCLASS" -> false,NeverDischarge,false,false,true + | "LSUBCLASS" -> true,make_strength_0(),false,false,true | _ -> anomaly "Unexpected string" in fun () -> - definition_body_red id stre c typ_opt red_option; + definition_body_red red_option id (local,stre) c typ_opt; if coe then begin Class.try_add_new_coercion id stre; message ((string_of_id id) ^ " is now a coercion") |