diff options
| author | Jasper Hugunin | 2018-10-25 13:58:03 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2018-11-08 17:20:31 -0800 |
| commit | 46f6b27f9808848556f88032cb2af0a8a9f6c017 (patch) | |
| tree | 22ef5639425cac0944be9b49ef6a990bcd9f82d3 /vernac | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
Standardize handling of Automatic Introduction.
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 10 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 5 |
2 files changed, 6 insertions, 9 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index f4b0015851..39919a141a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -146,7 +146,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps ?hook (ConstRef cst); id -let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = +let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then let hook _ _ vis gr = @@ -189,10 +189,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in ignore (Pfedit.by init_refine) else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () -let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len = +let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -275,7 +275,7 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype else if program_mode || refine || Option.is_empty term then - declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype + declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id @@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id else do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props len + cty k u ctx ctx' pri decl imps subst id props let named_of_rel_context l = let open Vars in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 8aa459729c..9019fa15d5 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -368,10 +368,7 @@ let rec_tac_initializer finite guard thms snl = | _ -> assert false let start_proof_with_initialization kind sigma decl recguard thms snl hook = - let intro_tac (_, (_, (ids, _))) = - Tacticals.New.tclMAP (function - | Name id -> Tactics.intro_mustbe_force id - | Anonymous -> Tactics.intro) (List.rev ids) in + let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> let rec_tac = rec_tac_initializer finite guard thms snl in |