Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

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

WhyML: put real effects in lambdas

parent eb3d5b87
......@@ -868,6 +868,7 @@ let create_fun_defn id ({l_expr = e; l_spec = c} as lam) recsyms =
let eff = if c.c_letrec <> 0 && c.c_variant = []
then eff_diverge e.e_effect else e.e_effect in
let spec = { c with c_effect = eff } in
let lam = { lam with l_spec = spec } in
let varm = spec_varmap e.e_varm spec in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
let varm = List.fold_left del_pv varm lam.l_args in
......
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