From 1488966795087e545626c198ba860704232e4bec Mon Sep 17 00:00:00 2001
From: Leon Gondelman <lgondelmann@gmail.com>
Date: Fri, 10 Feb 2017 13:32:53 +0100
Subject: [PATCH] coercions for '=': a temporary solution for x:63 = 0

---
 src/core/dterm.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/core/dterm.ml b/src/core/dterm.ml
index 1d2db6890..3e9638998 100644
--- a/src/core/dterm.ml
+++ b/src/core/dterm.ml
@@ -344,7 +344,6 @@ let dterm tuc ?loc node =
         end with Not_found ->
           Loc.error ?loc:dt.dt_loc FmlaExpected end
     | None -> dt
-
   and dterm_node loc node =
     let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
     match node with
@@ -356,6 +355,12 @@ let dterm tuc ?loc node =
        mk_dty (Some dty_int)
     | DTconst (Number.ConstReal _) ->
        mk_dty (Some dty_real)
+    | DTapp (ls, dtl) when ls_equal ls ps_equ ->
+       let dtyl, dty = specialize_ls ls in
+       let dtl = dty_unify_app_map ls dterm_expected (List.rev dtl) dtyl in
+       { dt_node = DTapp (ls, dtl);
+         dt_dty  = dty;
+         dt_loc  = loc }
     | DTapp (ls, dtl) ->
        let dtyl, dty = specialize_ls ls in
        { dt_node = DTapp (ls, dty_unify_app_map ls dterm_expected dtl dtyl);
-- 
GitLab