From ac945514d59d91e51a63149b39b472421e59e299 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 29 Dec 2018 14:00:40 +0000
Subject: Add separate termination_measure declarations

---
 src/parse_ast.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/parse_ast.ml')

diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 65b11373..20a0f48a 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -531,6 +531,7 @@ def =  (* Top-level definition *)
  | DEF_spec of val_spec (* top-level type constraint *)
  | DEF_default of default_typing_spec (* default kind and type assumptions *)
  | DEF_scattered of scattered_def (* scattered definition *)
+ | DEF_measure of id * pat * exp (* separate termination measure declaration *)
  | DEF_reg_dec of dec_spec (* register declaration *)
  | DEF_pragma of string * string * l
  | DEF_internal_mutrec of fundef list
-- 
cgit v1.2.3