diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 11:01:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 11:01:09 +0000 |
| commit | 23220a00beb45c8827370ab243df0d049b534183 (patch) | |
| tree | 5daae4c981a57bdfe6a64ee4d8461a97dbca1e32 /kernel | |
| parent | 5563b7abf1a93e42a99305b2e57d4e2924cef896 (diff) | |
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
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5812020f0..cfbd760d8 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) - |