expansion des constr purs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1665 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 4395aa53a5..3013c2c9b5 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -145,6 +145,12 @@ let rawconstr_of_prog p =
     (*i optimisation : let x = <constr> in e2  =>  e2[x<-constr] 
     | CC_letin (_,_,[id,_],CC_expr c,e2) ->
 	real_subst_in_constr [id,c] (trad e2)
+    | CC_letin (_,_,([_] as b),CC_expr e1,e2) ->
+	let (b',avoid',nenv') = push_vars avoid nenv b in
+      	let c1 = Detyping.detype avoid nenv e1 
+	and c2 = trad avoid' nenv' e2 in
+	let id = Name (fst (List.hd b')) in
+	RLetIn (dummy_loc, id, c1, c2)
     i*)
 
     | CC_letin (_,_,([_] as b),e1,e2) ->