From 23220a00beb45c8827370ab243df0d049b534183 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 11:01:09 +0000
Subject: On déplie les locaux dans les types plutôt que de les quantifier par
 un Let

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@982 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cooking.ml | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5812020f0e..cfbd760d83 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -127,18 +127,15 @@ let expmod_type oldenv modlist c =
 let abstract_constant ids_to_abs hyps (body,typ) =
   let abstract_once ((hyps,body,typ) as sofar) id =
     match hyps with
-      | [] -> 
+      | (hyp,c,t as decl)::rest when hyp = id ->
+	  let body' = match body with
+	    | None -> None
+	    | Some c -> Some (mkNamedLambda_or_LetIn decl c)
+	  in
+	  let typ' = mkNamedProd_wo_LetIn decl typ in
+	  (rest, body', typ')
+      | _ -> 
 	  sofar
-      | (hyp,c,t as decl)::rest ->
-	  if hyp <> id then 
-	    sofar
-	  else
-	    let body' = match body with
-	      | None -> None
-	      | Some c -> Some (mkNamedLambda_or_LetIn decl c)
-	    in
-	    let typ' = mkNamedProd_or_LetIn decl typ in
-	    (rest, body', typ')
   in
   let (_,body',typ') =
     List.fold_left abstract_once (hyps,body,typ) ids_to_abs in
@@ -150,4 +147,3 @@ let cook_constant env r =
   let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
   let hyps = map_named_context (expmod_constr env r.d_modlist) cb.const_hyps in
   abstract_constant r.d_abstract hyps (body,typ)
-
-- 
cgit v1.2.3