diff --git a/src/msph/tree.c b/src/msph/tree.c
index ec90d36..ca9a1de 100644
--- a/src/msph/tree.c
+++ b/src/msph/tree.c
@@ -534,7 +534,7 @@ tree_parse_forall(struct tree_parse *p, struct msph_tree *parent)
 		goto err;
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err);
-	EXPECT_CURR_TOKEN(p, TOK_COLON, MSPH_TREE_FORALL, goto err);
+	EXPECT_CURR_TOKEN(p, TOK_DOT, MSPH_TREE_FORALL, goto err);
 
 	EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err);
 	if ((fa->inner = tree_parse_tpexpr(p, T(fa))) == NULL)
@@ -751,6 +751,108 @@ err:
 	return (NULL);
 }
 
+struct msph_tree_dir *
+tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent)
+{
+	int res;
+	struct msph_tree_nomindecl *nomd;
+
+	EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL,
+	    return (NULL));
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, return (NULL));
+
+	if ((nomd = malloc(sizeof(*nomd))) == NULL) {
+		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
+		return (NULL);
+	}
+	T(nomd)->type = MSPH_TREE_NOMINDECL;
+	T(nomd)->parent = parent;
+	nomd->id = NULL;
+
+	if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL)
+		goto err;
+
+	return ((struct msph_tree_dir *)nomd);
+err:
+	free_the_tree(T(nomd));
+
+	return (NULL);
+}
+
+struct msph_tree_dir *
+tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent)
+{
+	int res;
+	struct msph_tree_membdecl *membd;
+
+	EXPECT_CURR_TOKEN(p, TOK_KW_MEMBER, MSPH_TREE_MEMBDECL,
+	    return (NULL));
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, return (NULL));
+
+	if ((membd = malloc(sizeof(*membd))) == NULL) {
+		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
+		return (NULL);
+	}
+	T(membd)->type = MSPH_TREE_NOMINDECL;
+	T(membd)->parent = parent;
+	membd->id = NULL;
+	membd->tp = NULL;
+
+	if ((membd->id = tree_parse_ident(p, T(membd))) == NULL)
+		goto err;
+
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err);
+	EXPECT_CURR_TOKEN(p, TOK_COLON, MSPH_TREE_MEMBDECL,
+	    goto err);
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err);
+
+	if ((membd->tp = tree_parse_tpexpr(p, T(membd))) == NULL)
+		goto err;
+
+	return ((struct msph_tree_dir *)membd);
+err:
+	free_the_tree(T(membd));
+
+	return (NULL);
+}
+
+struct msph_tree_dir *
+tree_parse_assert(struct tree_parse *p, struct msph_tree *parent)
+{
+	int res;
+	struct msph_tree_assert *ass;
+
+	EXPECT_CURR_TOKEN(p, TOK_KW_ASSERT, MSPH_TREE_ASSERT,
+	    return (NULL));
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, return (NULL));
+
+	if ((ass = malloc(sizeof(*ass))) == NULL) {
+		MSPH_ERR(CTX(p), MSPH_ERR_SYS);
+		return (NULL);
+	}
+	T(ass)->type = MSPH_TREE_ASSERT;
+	T(ass)->parent = parent;
+	ass->ltp = NULL;
+	ass->rtp = NULL;
+
+	if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL)
+		goto err;
+
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
+	EXPECT_CURR_TOKEN(p, TOK_SUB, MSPH_TREE_ASSERT,
+	    goto err);
+	EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err);
+
+	if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL)
+		goto err;
+
+	return ((struct msph_tree_dir *)ass);
+err:
+	free_the_tree(T(ass));
+
+	return (NULL);
+}
+
 static void
 free_the_tree(struct msph_tree *tree)
 {
@@ -758,4 +860,3 @@ free_the_tree(struct msph_tree *tree)
 	SPHO_POSTCOND((void *)tree == (void *)free);
 }
 
-