with
| Cic.MutInd (uri, tyno, _) ->
(GrafiteAst.Type (uri, tyno) :: types)
- | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
+ | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
in
let types = List.fold_left disambiguate [] types in
GrafiteAst.Decompose (loc, types, what, names)
in
try
aux paths
- with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
+ with Unix.Unix_error _ -> raise (UnableToInclude path)
;;
let eval_command opts status cmd =
"name/uri. This should be fixed!")
| _-> command_error "You can't Qed an incomplete theorem"
in
- let suri = UriManager.string_of_uri uri in
if metasenv <> [] then
command_error "Proof not completed! metasenv is not empty!";
let name = UriManager.name_of_uri uri in