From 7c281301637f783beaec858a5fee665e99a6813b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 11 Mar 2013 21:35:19 +0000
Subject: Allowing (Co)Fixpoint to be defined local and Let-style.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/vernacexpr.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index a1eca85bc1..cb6b74bcc9 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -240,8 +240,8 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
   | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list
+  | VernacFixpoint of locality * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of locality * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
 
-- 
cgit v1.2.3