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

1 files changed, 7 insertions, 0 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c9d44e3dc..5b4e8e7cf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -583,6 +583,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
+    | RLetPattern (loc, c, p) ->
+	(* Just use cases typing *)
+	let j = 
+	  pretype tycon env evdref lvar 
+	    (RCases (loc, None, [c], [p]))
+	in j
+	
     | RCases (loc,po,tml,eqns) ->
 	Cases.compile_cases loc
 	  ((fun vtyc env -> pretype vtyc env evdref lvar),evdref)