diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 59 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 |
2 files changed, 23 insertions, 38 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index d93fcc0950..da3a119a79 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -314,18 +314,21 @@ type section_variable_entry = type variable_declaration = DirPath.t * section_variable_entry -let cache_variable (_,o) = - match o with - | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(path,d),kind) -> +(* This object is only for things which iterate over objects to find + variables (only Prettyp.print_context AFAICT) *) +let inVariable : unit -> obj = + declare_object { (default_object "VARIABLE") with + classify_function = (fun () -> Dispose)} + +let declare_variable ~name ~kind (path,d) = (* Constr raisonne sur les noms courts *) - if Decls.variable_exists id then - raise (AlreadyDeclared (None, id)); + if Decls.variable_exists name then + raise (AlreadyDeclared (None, name)); let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;univs;poly;impl} -> - let () = Global.push_context_set poly univs in - let () = Global.push_named_assum (id,typ) in + let () = declare_universe_context ~poly univs in + let () = Global.push_named_assum (name,typ) in let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in impl, true, poly, univs | SectionLocalDef (de) -> @@ -337,47 +340,29 @@ let cache_variable (_,o) = let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.proof_entry_universes with - | Monomorphic_entry uctx -> false, uctx - | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx + | Monomorphic_entry uctx -> false, uctx + | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (* We must declare the universe constraints before type-checking the term. *) - let () = Global.push_context_set (not poly) univs in + let () = declare_universe_context ~poly univs in let se = { secdef_body = body; secdef_secctx = de.proof_entry_secctx; secdef_feedback = de.proof_entry_feedback; secdef_type = de.proof_entry_type; } in - let () = Global.push_named_def (id, se) in + let () = Global.push_named_def (name, se) in Decl_kinds.Explicit, de.proof_entry_opaque, - poly, univs in - Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty id) (GlobRef.VarRef id); - add_section_variable ~name:id ~kind:impl ~poly univs; - Decls.(add_variable_data id {path;opaque;univs;poly;kind}) - -let discharge_variable (_,o) = match o with - | Inr (id,_,_) -> - if Decls.variable_polymorphic id then None - else Some (Inl (Decls.variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable ~name ~kind obj = - let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in + poly, univs + in + Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); + add_section_variable ~name ~kind:impl ~poly univs; + Decls.(add_variable_data name {path;opaque;univs;poly;kind}); + add_anonymous_leaf (inVariable ()); Impargs.declare_var_implicits name; - Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name); - oname + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = diff --git a/tactics/declare.mli b/tactics/declare.mli index f2d23fb319..3edb3f29cd 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -36,7 +36,7 @@ val declare_variable : name:variable -> kind:Decls.logical_kind -> variable_declaration - -> Libobject.object_name + -> unit (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) |