Commit 29a88d32 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated ROADMAP; cleaning up

parent 3113cea0
......@@ -226,9 +226,7 @@ See manual Section xx
* (JCF) ameliorer why3doc
- DONE rajouter la production des liens
- produire un index.html
- entree makefile pour produire la bibliotheque standard de Why3 en HTML
(pour mettre sur le site Web)
- DONE produire un index.html
* DONE provers
- DONE (CLAUDE) Ensure that we kill a prover after some time
......@@ -2186,15 +2186,7 @@ let add_types uc dl =
| Ty.Tyvar _ ->
| Ty.Tyapp (ts, tyl) ->
let y = ts.ts_name.id_string in
let n =
if Mstr.mem y def then begin
visit y; of_option (Hashtbl.find nregions y)
end else
(get_mtsymbol ts).mt_regions
let n = (get_mtsymbol ts).mt_regions in
let rl = regions_tyapp ts n tyl in
List.iter (fun r -> declare_region_type r.R.r_ty) rl;
List.iter visit_type tyl
Supports Markdown
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