diff options
| author | Gaëtan Gilbert | 2019-08-23 23:06:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-08-23 23:06:41 +0200 |
| commit | 2c36189fb8c433fa1d3adff4ea2c52a7b1ff29cc (patch) | |
| tree | 4a201b720331128dfe60157057a8b95f250389b4 /tactics | |
| parent | b0a9cbeaf0530533008aa99246164b2bad896c5a (diff) | |
| parent | 451acd6ca6a9ce5b86622fb42085eb19e23d6665 (diff) | |
Merge PR #10665: [api] Move handling of variable implicit data to impargs
Reviewed-by: SkySkimmer
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 9 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 1 |
3 files changed, 5 insertions, 7 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 391524ebda..c280760e84 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -300,7 +300,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) @@ -317,7 +317,6 @@ let declare_variable ~name ~kind d = | SectionLocalAssum {typ;univs;poly;impl} -> 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 | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a @@ -342,14 +341,14 @@ let declare_variable ~name ~kind d = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (name, se) in - Decl_kinds.Explicit, de.proof_entry_opaque, + Glob_term.Explicit, de.proof_entry_opaque, poly in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); - add_section_variable ~name ~kind:impl ~poly; + add_section_variable ~name ~poly; Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); - Impargs.declare_var_implicits name; + Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) (** Declaration of inductive blocks *) diff --git a/tactics/declare.mli b/tactics/declare.mli index 89b41076f7..4ae9f6c7ae 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = | DefinitionEntry of 'a Proof_global.proof_entry diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a3a88df21e..61e0e41eb9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -258,7 +258,6 @@ type equation_kind = exception NoEquationFound open Glob_term -open Decl_kinds open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) |