From d4567298bdf4e83f44fc1567448d68677eb8e9ca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Oct 2000 13:40:04 +0000
Subject: Ajout LetIn dans prim_extractor

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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index aebc76539c..d7b67ba395 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -472,6 +472,10 @@ let prim_extractor subfun vl pft =
 	   | IsProd (_,ty,_) ->
 	       let cty = subst_vars vl ty in
 	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | IsLetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | { ref = Some (Prim { name = Intro_after; newids = [id]}, [spf]) } -> 
@@ -479,6 +483,10 @@ let prim_extractor subfun vl pft =
 	   | IsProd (_,ty,_) ->
 	       let cty = subst_vars vl ty in
 	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | IsLetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | {ref=Some(Prim{name=Intro_replacing;hypspecs=[id]},[spf]) } ->
@@ -486,6 +494,10 @@ let prim_extractor subfun vl pft =
 	   | IsProd (_,ty,_) ->
 	       let cty = subst_vars vl ty in
 	       mkLambda (Name id, cty, subfun (id::vl) spf)
+	   | IsLetIn (_,b,ty,_) ->
+	       let cb = subst_vars vl b in
+	       let cty = subst_vars vl ty in
+	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
 	
     | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> 
-- 
cgit v1.2.3