From 7f99d8016ced351efd0a42598a9d18001b2e4d46 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 31 Jan 2008 15:19:22 +0000
Subject: Finish let| implementation and document it

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml  | 2 +-
 kernel/term.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index ad4bd2bda2..45cd2fb0e0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -24,7 +24,7 @@ type metavariable = int
 (* This defines the strategy to use for verifiying a Cast *)
 
 (* This defines Cases annotations *)
-type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
     style     : case_style }
diff --git a/kernel/term.mli b/kernel/term.mli
index f71207c5e1..2c6e7f0b48 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -40,7 +40,7 @@ type existential_key = int
 type metavariable = int
 
 (*s Case annotation *)
-type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
     style     : case_style }
-- 
cgit v1.2.3