Commit 54f861c5 authored by Francois Bobot's avatar Francois Bobot
Browse files

sorry

parent 3fb9edf5
......@@ -58,8 +58,8 @@ let rec report fmt = function
fprintf fmt "syntax error"
| Typing.Error e ->
Typing.report fmt e
| Theory.Context.UnknownIdent i ->
fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
(* | Theory.Context.UnknownIdent i ->
fprintf fmt "anomaly: unknownident %s" i.Ident.id_short*)
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
......
......@@ -2,7 +2,7 @@ open Theory
let elt a =
let rec aux first_level acc d = match first_level, d.d_node with
| _,Duse t -> Context.ctxt_fold (aux false) acc t.th_ctxt
| _,Duse t -> Context.ctxt_fold (aux false) (d::acc) t.th_ctxt
| false,Dprop (Pgoal,_,_) -> acc
| false,Dprop (Plemma,i,f) -> (create_prop Paxiom (Ident.id_dup i) f)::acc
| _ -> d::acc
......
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