diff options
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 ad6c4236e..8f36fc79f 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 95cfd73a0..a23b1b64a 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 7694869a5..be3fb7c2c 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 |