diff options
| author | Matthieu Sozeau | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /toplevel/command.ml | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 582dde30d3..9b650f859a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -333,7 +333,7 @@ let prepare_param = function let rec check_anonymous_type ind = let open Glob_term in match ind with - | GSort (_, GType None) -> true + | GSort (_, GType []) -> true | GProd (_, _, _, _, e) | GLetIn (_, _, _, e) | GLambda (_, _, _, _, e) @@ -570,7 +570,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType None)) ar; + ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl |