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

corrigee sauf que Duse n'est plus conserve apres l'applatissement

parent 4e3490c3
......@@ -2,14 +2,13 @@ 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
(* Pourquoi ce rev? *)
let r = (aux true [] a) in
Format.printf "flat %a : %a@\n" Pretty.print_decl a Pretty.print_decl_list r;
(*Format.printf "flat %a : %a@\n" Pretty.print_decl a Pretty.print_decl_list r;*)
......@@ -48,7 +48,7 @@ and substt env d = t_map (replacet env) (replacep env) d
and substp env d = f_map (replacet env) (replacep env) d
let fold _ env ctxt d =
Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;
(* Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
match d.d_node with
| Dlogic [l] -> begin
match l 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