Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

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

typage de PPnamed

parent 022bd3c3
......@@ -381,7 +381,7 @@ and dfmla =
| Fif of dfmla * dfmla * dfmla
| Flet of dterm * string * dfmla
(* | Fcase of dterm * (pattern * dfmla) list *)
| Fnamed of string * fmla
| Fnamed of string * dfmla
and dtrigger =
| TRterm of dterm
......@@ -481,8 +481,9 @@ and dfmla env e = match e.pp_desc with
Flet (e1, x, e2)
| PPmatch _ ->
assert false (* TODO *)
| PPnamed _ ->
assert false (* TODO *)
| PPnamed (x, f1) ->
let f1 = dfmla env f1 in
Fnamed (x, f1)
| PPvar _ ->
assert false (* TODO *)
| PPconst _ | PPprefix (PPneg, _) ->
......@@ -558,6 +559,7 @@ and fmla env = function
let f2 = fmla env f2 in
f_let v e1 f2
| Fnamed (x, f1) ->
let f1 = fmla env f1 in
f_label_add x f1
(** Typing declarations, that is building environments. *)
......
......@@ -4,7 +4,7 @@
theory A
use import prelude.Int
axiom A :
let x = 2+2 in x*x = 16
F : let x = 2+2 in G : x*x = 16
end
theory TreeForest
......
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