Commit 08d1a75c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Decl: check positivity in conclusion of inductive clauses [#18006]

parent 8388828a
......@@ -521,7 +521,7 @@ let create_ind_decl s idl =
match g.t_node with
| Tapp (s, tl) when ls_equal s ps ->
List.iter2 check_tl ps.ls_args tl;
(try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
(try ignore (List.for_all (f_pos_ps sps (Some true)) (g::cls))
with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
(* check for unbound type variables *)
let gtv = t_ty_freevars Stv.empty g in
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment