From 9dae3bc45e05fc3be987f79b5098248a9d725ce2 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 12 Mar 2001 09:34:13 +0000
Subject: debut let in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1450 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extraction.ml | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 8233b9f41c..4da0bd19e3 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -339,17 +339,23 @@ and extract_term c =
 	     | Tarity -> assert false (* Cf. precondition *)
 	     | Tprop -> Eprop)
       | IsConst (sp,_) ->
-	  Emlterm (MLglob (ConstRef sp)) (* TODO eta-expansion *)
+	  Emlterm (MLglob (ConstRef sp))
       | IsMutConstruct (cp,_) ->
-	  Emlterm (MLglob (ConstructRef cp))
+	  Emlterm (MLglob (ConstructRef cp)) (* TODO eta-expansion *)
       | IsMutCase _ ->
 	  failwith "todo"
       | IsFix _ ->
 	  failwith "todo"
       | IsLetIn (n, c1, t1, c2) ->
-	  failwith "todo"
-	    (*i	  (match get_arity env t1 with
-	      | Some (Prop Null) -> *)
+	  let id = id_of_name n in
+	  let env' = push_rel (n,Some c1,t1) env in
+	  (match get_arity env t1 with
+	     | Some (Prop Null) -> 
+		 extract_rec env' ((Tprop,id)::ctx) c2
+	     | Some _ ->
+		 failwith "todo" (* extract_rec env' *)
+	     | _ ->
+		 failwith "todo")
       | IsCast (c, _) ->
 	  extract_rec env ctx c
       | IsMutInd _ | IsProd _ | IsSort _ | IsVar _ 
@@ -390,7 +396,7 @@ and extract_constr_with_type c t =
     | Some _ -> 
 	(match extract_type genv [] c with
 	   | Tprop -> Eprop
-	   | Tarity -> Emltype(Miniml.Tarity, [], []) (* any other arity *)
+	   | Tarity -> Emltype (Miniml.Tarity, [], []) (* any other arity *)
 	   | Tmltype (t, sign, fl) -> Emltype (t, sign, fl))
     | None -> 
 	extract_term c
-- 
cgit v1.2.3