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 /pretyping/pretyping.ml | |
| 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 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8c4dbfd984..69aee0a602 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -440,15 +440,15 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let k = Evar_kinds.MatchingVar (someta,n) in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } - | GHole (loc, k, None) -> + | GHole (loc, k, naming, None) -> let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } - | GHole (loc, k, Some arg) -> + | GHole (loc, k, _naming, Some arg) -> let ty = match tycon with | Some ty -> ty @@ -910,7 +910,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type resolve_tc valcon env evdref lvar = function - | GHole (loc, knd, None) -> + | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = @@ -926,7 +926,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function utj_type = s } | None -> let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in - { utj_val = e_new_evar env evdref ~src:(loc, knd) (mkSort s); + { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) | c -> let j = pretype resolve_tc empty_tycon env evdref lvar c in |