diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/command.ml | 17 | ||||
-rw-r--r-- | toplevel/command.mli | 22 | ||||
-rw-r--r-- | toplevel/record.ml | 2 | ||||
-rw-r--r-- | toplevel/record.mli | 5 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 13 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 15 |
6 files changed, 31 insertions, 43 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 234910af0..c6a038c3b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -83,7 +83,7 @@ let declare_definition red_option ident (local,n) c typopt = | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type) in - let sp = declare_variable ident (Lib.cwd(), c, n) in + let _ = declare_variable ident (Lib.cwd(), c, n) in if_verbose message ((string_of_id ident) ^ " is defined"); if Pfedit.refining () then msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ @@ -110,22 +110,25 @@ let declare_assumption ident n c = let c = interp_type Evd.empty (Global.env()) c in match n with | NeverDischarge -> - let _ = declare_constant ident (ParameterEntry c, NeverDischarge) in - assumption_message ident + let r = declare_constant ident (ParameterEntry c, NeverDischarge) in + assumption_message ident; + ConstRef r | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin - let _ = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in + let r = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ - str" is not visible from current goals") + str" is not visible from current goals"); + VarRef ident end else - let _ = declare_constant ident (ParameterEntry c, NeverDischarge) in + let r = declare_constant ident (ParameterEntry c, NeverDischarge) in assumption_message ident; if_verbose msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); + ConstRef r | NotDeclare -> anomalylabstrm "Command.hypothesis_def_var" (str "Strength NotDeclare not for Variable, only for Let") @@ -220,7 +223,7 @@ let eq_la (id,ast) (id',ast') = id = id' & alpha_eq(ast,ast') let extract_coe lc = List.fold_right - (fun (id,addcoe,t) (l1,l2) -> + (fun (addcoe,(id,t)) (l1,l2) -> ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[]) let extract_coe_la_lc = function diff --git a/toplevel/command.mli b/toplevel/command.mli index 474fe9202..ea6c97e0e 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,32 +21,12 @@ open Library functions of [Declare]; they return an absolute reference to the defined object *) -(*i -val constant_entry_of_com : - Coqast.t * Coqast.t option * bool -> Safe_typing.constant_entry - -val declare_global_definition : - Names.identifier -> - Safe_typing.constant_entry -> - Declare.strength -> bool -> Nametab.global_reference - -val definition_body : identifier -> bool * strength -> - Coqast.t -> Coqast.t option -> global_reference -i*) - val declare_definition : Tacred.red_expr option -> identifier -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference val syntax_definition : identifier -> Coqast.t -> unit -(*i -val hypothesis_def_var : bool -> identifier -> strength -> Coqast.t - -> global_reference - -val parameter_def_var : identifier -> Coqast.t -> constant -i*) - -val declare_assumption : identifier -> strength -> Coqast.t -> unit +val declare_assumption : identifier -> strength -> Coqast.t -> global_reference val build_mutual : Vernacexpr.inductive_expr list -> bool -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index c7907b167..10b9c42da 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -209,7 +209,7 @@ let declare_projections indsp coers fields = (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) -let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = +let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) = let coers,fs = List.split cfs in let nparams = List.length ps in let idps = List.map fst ps in diff --git a/toplevel/record.mli b/toplevel/record.mli index 1419b9c3c..90b40020e 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -12,6 +12,7 @@ open Names open Term open Sign +open Vernacexpr (*i*) (* [declare_projections ref coers params fields] declare projections of @@ -22,5 +23,5 @@ val declare_projections : inductive -> bool list -> rel_context -> constant option list val definition_structure : - bool * identifier * (identifier * Genarg.constr_ast) list * - (bool * Vernacexpr.local_decl_expr) list * identifier * sorts -> unit + identifier with_coercion * (identifier * Genarg.constr_ast) list * + (local_decl_expr with_coercion) list * identifier * sorts -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d8de77b9..9c11ae7cb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -307,7 +307,10 @@ let vernac_exact_proof c = let vernac_assumption kind l = let stre = interp_assumption kind in - List.iter (fun (id,c) -> declare_assumption id stre c) l + List.iter + (fun (is_coe,(id,c)) -> + let r = declare_assumption id stre c in + if is_coe then Class.try_add_new_coercion r stre) l let vernac_inductive f indl = build_mutual indl f @@ -321,12 +324,12 @@ let vernac_scheme = build_scheme (**********************) (* Gallina extensions *) -let vernac_record iscoe struc binders sort nameopt cfs = +let vernac_record struc binders sort nameopt cfs = let const = match nameopt with - | None -> add_prefix "Build_" struc + | None -> add_prefix "Build_" (snd struc) | Some id -> id in let s = Astterm.interp_sort sort in - Record.definition_structure (iscoe,struc,binders,cfs,const,s) + Record.definition_structure (struc,binders,cfs,const,s) (* Sections *) @@ -876,7 +879,7 @@ let interp c = match c with | VernacScheme l -> vernac_scheme l (* Gallina extensions *) - | VernacRecord (coe,id,bl,s,idopt,fs) -> vernac_record coe id bl s idopt fs + | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacBeginSection id -> vernac_begin_section id | VernacEndSection id -> vernac_end_section id | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 365192599..f1bd6ed52 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -140,12 +140,13 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *) type sort_expr = t -type simple_binders = identifier * constr_ast -type constructor_expr = identifier * coercion_flag * constr_ast +type simple_binder = identifier * constr_ast +type 'a with_coercion = coercion_flag * 'a +type constructor_expr = simple_binder with_coercion type inductive_expr = - identifier * simple_binders list * constr_ast * constructor_expr list + identifier * simple_binder list * constr_ast * constructor_expr list type fixpoint_expr = - identifier * simple_binders list * constr_ast * constr_ast + identifier * simple_binder list * constr_ast * constr_ast type cofixpoint_expr = identifier * constr_ast * constr_ast @@ -180,15 +181,15 @@ type vernac_expr = constr_ast * bool * Proof_type.declaration_hook | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option | VernacExactProof of constr_ast - | VernacAssumption of assumption_kind * simple_binders list + | VernacAssumption of assumption_kind * simple_binder with_coercion list | VernacInductive of inductive_flag * inductive_expr list | VernacFixpoint of fixpoint_expr list | VernacCoFixpoint of cofixpoint_expr list | VernacScheme of (identifier * bool * qualid located * sort_expr) list (* Gallina extensions *) - | VernacRecord of coercion_flag * identifier * simple_binders list - * sort_expr * identifier option * (coercion_flag * local_decl_expr) list + | VernacRecord of identifier with_coercion * simple_binder list + * sort_expr * identifier option * local_decl_expr with_coercion list | VernacBeginSection of identifier | VernacEndSection of identifier | VernacRequire of |