From 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 10 Sep 2000 07:19:28 +0000
Subject: Ajout d'un LetIn primitif. Abstraction de constr via kind_of_constr
 dans une bonne partie du code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/PPConstr.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'syntax')

diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index ad74cd462e..25f8a2c7f7 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -129,6 +129,7 @@ Syntax constr
   | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)]
       -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
 
+  | letin [<<[$x = $A] $B>>] -> [ [ <hov 0> "[" $x ":=" $A "]" [0 1] $B:E ] ]
 
   | pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)]
   | prodlist  [(PRODLIST $c $b)]
-- 
cgit v1.2.3