let canonical_context' =
List.map
(function
- _,None -> None
- | _,Some (`Declaration d)
- | _,Some (`Hypothesis d) ->
+ None -> None
+ | Some (`Declaration d)
+ | Some (`Hypothesis d) ->
(match d with
{K.dec_name = Some n ; K.dec_type = t} ->
Some (Cic.Name n, Cic.Decl (deannotate t))
| _ -> assert false)
- | _,Some (`Definition d) ->
+ | Some (`Definition d) ->
(match d with
{K.def_name = Some n ; K.def_term = t} ->
Some (Cic.Name n, Cic.Def (deannotate t))
| _ -> assert false)
- | _,Some (`Proof d) ->
+ | Some (`Proof d) ->
(match d with
{K.proof_name = Some n } ->
Some (Cic.Name n, Cic.Def (proof2cic deannotate d))