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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 4 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index ad6c4236ef..8f36fc79fe 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -115,7 +115,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> - let t = CHole (Loc.ghost, None, None) in + let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -223,7 +223,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, None) :: props), rest + (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/toplevel/command.ml b/toplevel/command.ml index 95cfd73a04..a23b1b64af 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -53,7 +53,7 @@ let rec under_binders env f n c = let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) - | CHole (loc, k, _) -> + | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", diff --git a/toplevel/record.ml b/toplevel/record.ml index 7694869a50..be3fb7c2cc 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -86,7 +86,7 @@ let compute_constructor_level evars env l = let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) - | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, None)) + | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, Misctypes.IntroAnonymous, None)) let binders_of_decls = List.map binder_of_decl |