Commit aba3c7c3 authored by Francois Bobot's avatar Francois Bobot
Browse files

Pourquoi Theory.Context n'est pas un module accessible alors que apres open Theory Context l'est?

parent 54f861c5
......@@ -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*)
| 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) (d::acc) t.th_ctxt
| _,Duse t -> Context.ctxt_fold (aux false) 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