From cd21f033922b22f855111e171ece9591009cf15b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 17 Jan 2008 16:04:42 +0000
Subject: Add new LetPattern construct to replace dest. syntax: let| pat := t
 in b is backwards compatible. Update CHANGES with things i've done.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 69d5ad67a9..eb69e12257 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -722,6 +722,15 @@ let rec extern inctx scopes vars r =
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
+  | RLetPattern (loc,(tm,_), eqn) ->
+      let p, c = 
+	match extern_eqn false scopes vars eqn with
+	    (loc,[loc',[p]], c) -> p,c
+	  | _ -> assert false
+      in
+      let t = extern inctx scopes vars tm in
+	CLetPattern(loc, p, t, c)
+
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
         (Option.map (fun _ -> na) typopt,
-- 
cgit v1.2.3