diff options
| author | Hugo Herbelin | 2014-09-30 09:13:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-30 09:30:53 +0200 |
| commit | 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f (patch) | |
| tree | 53478ded9dfb8108402d7f45fa1300edd1569a20 /tactics | |
| parent | 2bbf1305a080667d8547c44b2684010aba3d8d45 (diff) | |
Add syntax for naming new goals in refine: writing ?[id] instead of _
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 34f5b52ebf..cb15bb94c0 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -596,7 +596,8 @@ let subst_var_with_hole occ tid t = else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true), None))) + Evar_kinds.QuestionMark(Evar_kinds.Define true), + Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t @@ -607,13 +608,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) -> + | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; GHole (Loc.make_loc (!locref,0), - Evar_kinds.QuestionMark(Evar_kinds.Define true),s)) + Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 30ee5c5147..bd20741399 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1766,7 +1766,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2); (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CHole (Loc.ghost, None, None) +let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) let proper_projection r ty = let ctx, inst = decompose_prod_assum ty in |