diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 8 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 1 |
2 files changed, 4 insertions, 5 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index e093a27728..cdbb3d41d9 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -317,7 +317,7 @@ 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 + let impl = if impl then Glob_term.Implicit else Glob_term.Explicit in impl, true, poly | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a @@ -342,14 +342,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/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) |