diff --git a/client/F.ml b/client/F.ml
index a064d0c48066c35796d1c039dd562b4ab3dee23c..5fc2eb884762e14677334bca2f20ed8a548a0a15 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -87,7 +87,7 @@ type ('a, 'b) term =
   | Annot of loc * ('a, 'b) term * ('a, 'b) typ
   | Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
   | App of loc * ('a, 'b) term * ('a, 'b) term
-  | Let of loc * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
+  | Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
   | TyAbs of loc * 'b * ('a, 'b) term
   | TyApp of loc * ('a, 'b) term * ('a, 'b) typ
   | Tuple of loc * ('a, 'b) term list
@@ -99,6 +99,8 @@ type ('a, 'b) term =
   | Refl of loc * ('a,'b) typ
   | Use of loc * ('a,'b) term * ('a,'b) term
 
+and rec_status = Recursive | Non_recursive
+
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
 and ('a,'b) pattern =
@@ -222,11 +224,11 @@ module TypeInTerm : DeBruijn.TRAVERSE
         let t1' = trav env t1
         and t2' = trav env t2 in
         App (pos, t1', t2')
-    | Let (pos, x, ty, t1, t2) ->
+    | Let (pos, rec_, x, ty, t1, t2) ->
         let ty' = trav_ty env ty in
         let t1' = trav env t1
         and t2' = trav env t2 in
-        Let (pos, x, ty', t1', t2')
+        Let (pos, rec_, x, ty', t1', t2')
     | TyAbs (pos, x, t) ->
         let env, x = extend env x in
         let t' = trav env t in
diff --git a/client/F.mli b/client/F.mli
index 1ceb0a4248a5041c3f3fc8331ffcb0ea1fea9c01..eed4d7f491fb3de82342b63aa29f9340ace6a512 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -88,7 +88,7 @@ type ('a, 'b) term =
   | Annot of loc * ('a, 'b) term * ('a, 'b) typ
   | Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
   | App of loc * ('a, 'b) term * ('a, 'b) term
-  | Let of loc * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
+  | Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
   | TyAbs of loc * 'b * ('a, 'b) term
   | TyApp of loc * ('a, 'b) term * ('a, 'b) typ
   | Tuple of loc * ('a, 'b) term list
@@ -100,6 +100,8 @@ type ('a, 'b) term =
   | Refl of loc * ('a,'b) typ
   | Use of loc * ('a,'b) term * ('a,'b) term
 
+and rec_status = Recursive | Non_recursive
+
 and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
 
 and ('a,'b) pattern =
diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index 21bfcbefcc7727afcb86120bed4bc912bac12d83..7d5b92264a11b0657c55dc379353090ceb85b9a1 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -61,9 +61,13 @@ let rec translate_term env (t : F.nominal_term) : P.term =
       P.Abs (x_annot, self env t)
   | F.App (_, t1, t2) ->
       P.App (self env t1, self env t2)
-  | F.Let (_, x, ty, t, u) ->
+  | F.Let (_, rec_, x, ty, t, u) ->
+      let rec_ = match rec_ with
+      | F.Recursive -> P.Recursive
+      | F.Non_recursive -> P.Non_recursive
+      in
       let x_annot = P.PAnnot (P.PVar x, annot env ty) in
-      P.Let (P.Non_recursive, x_annot, self env t, self env u)
+      P.Let (rec_, x_annot, self env t, self env u)
   | F.TyAbs (_, x, t) ->
       let alpha = new_tyvar () in
       P.TyAbs (alpha, self ((x, alpha) :: env) t)
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 76f1052c8c1d6b3971db69cb0e09cbaae9cb2967..332d1c782e7df6daacaa1683caa45d9245594a09 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -384,10 +384,14 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
       let ty1, ty2 = as_arrow ~loc (typeof env t) in
       enforce_equal ~loc env (typeof env u) ty1;
       ty2
-  | Let (loc, x, ty, t, u) ->
-      enforce_equal ~loc env (typeof env t) ty;
-      let env = extend_with_tevar env x ty in
-      typeof env u
+  | Let (loc, rec_, x, ty, t, u) ->
+      let env_with_x = extend_with_tevar env x ty in
+      let def_env = match rec_ with
+        | Non_recursive -> env
+        | Recursive -> env_with_x
+      in
+      enforce_equal ~loc def_env (typeof def_env t) ty;
+      typeof env_with_x u
   | TyAbs (_, (), t) ->
       TyForall ((), typeof (extend_with_tyvar env) t)
   | TyApp (loc, t, ty2) ->
diff --git a/client/Infer.ml b/client/Infer.ml
index 742a71be1de4f0b4bb2c99aa3e7e14fd8fd5a2a4..0e57b3d314cbeb14e7619eae9f29155f75d08de1 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -130,7 +130,7 @@ let flet ~loc (x, ty, t, u) =
   | F.Var (_, y) when smart && x = y ->
       u
   | t ->
-      F.Let (loc, x, ty, t, u)
+      F.Let (loc, F.Non_recursive, x, ty, t, u)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -372,7 +372,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
          produced. *)
       let sch tyvars =
         List.fold_right (fun alpha sch -> F.TyForall (alpha, sch)) tyvars ty in
-      F.Let (loc, x, sch a, F.ftyabs ~loc a t',
+      F.Let (loc, F.Non_recursive, x, sch a, F.ftyabs ~loc a t',
              flet ~loc (x, sch b, coerce ~loc a b (F.Var (loc, x)),
                         u'))