diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-20 21:01:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-20 21:01:34 +0200 |
| commit | 69a35378d37b8eb7e1019d24ab5e0fd27f25b6bc (patch) | |
| tree | 55a6d17a0de13244a6454263ae3de6bc5b3c2374 /tactics | |
| parent | 1af95525a2a791889e6d72dfc150ff8f09a21e21 (diff) | |
More standard naming for the Imparg.with_implicits function.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ebbd09cb8..9d08ada60 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4871,7 +4871,7 @@ let abstract_subproof id gk tac = (** ppedrot: seems legit to have abstracted subproofs as local*) Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in - let cst = Impargs.with_implicits cst () in + let cst = Impargs.with_implicit_protection cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in |