diff options
| author | Hugo Herbelin | 2017-02-01 15:56:45 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 12:22:21 +0100 |
| commit | f9a4ca41bc1313300f5f9b9092fe24825f435706 (patch) | |
| tree | f2c6f100a01e26614a5ff6e7fe7471c7356b9de4 /vernac | |
| parent | 71cd2838bf3eb23a8f29df973d8012ebe2ec77b0 (diff) | |
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 6 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index cdc1c88e63..8244ee5346 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -55,7 +55,7 @@ let rec under_binders env sigma 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) + | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c) | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then @@ -416,7 +416,7 @@ let rec check_anonymous_type ind = match ind with | GSort (_, GType []) -> true | GProd (_, _, _, _, e) - | GLetIn (_, _, _, e) + | GLetIn (_, _, _, _, e) | GLambda (_, _, _, _, e) | GApp (_, e, _) | GCast (_, e, _) -> check_anonymous_type e @@ -560,7 +560,7 @@ let check_named (loc, na) = match na with let check_param = function -| CLocalDef (na, _) -> check_named na +| CLocalDef (na, _, _) -> check_named na | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false diff --git a/vernac/record.ml b/vernac/record.ml index a6c8f8b369..51d89f1551 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -108,7 +108,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = | _ -> () in List.iter - (function CLocalDef (b, _) -> error default_binder_kind b + (function CLocalDef (b, _, _) -> error default_binder_kind b | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls | CLocalPattern (loc,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps |