Commit ae198377 authored by Andrei Paskevich's avatar Andrei Paskevich

minor fix

parent ad3f6c83
......@@ -641,8 +641,8 @@ let find_constructors kn ts =
let find_inductive_cases kn ps =
match (Mid.find ps.ls_name kn).d_node with
| Dind (_, dl) -> List.assq ps dl
| Dlogic _ | Ddata _ -> []
| Dtype _ | Dparam _ | Dprop _ -> assert false
| Dlogic _ | Dparam _ | Ddata _ -> []
| Dtype _ | Dprop _ -> assert false
let find_logic_definition kn ls =
match (Mid.find ls.ls_name kn).d_node with
......
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