diff options
| author | letouzey | 2001-11-12 10:00:49 +0000 |
|---|---|---|
| committer | letouzey | 2001-11-12 10:00:49 +0000 |
| commit | da33e695040678d74622213af2cd43d32140d186 (patch) | |
| tree | 603b9369b34539973a609c85a7c8c0c178758700 | |
| parent | 9d478de763bbc2088cd7250309b2a811a5bf8c57 (diff) | |
suite refonte extraction.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2182 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/extraction.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 368b41e3c7..a16642ca79 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -481,7 +481,9 @@ and signature_rec env c args = signature_rec env d (Array.to_list args' @ args) | Rel n -> (match lookup_rel n env with - | (_,Some t,_) -> signature_rec env (lift n t) args + | (_,Some t,_) -> + let c' = whd_betaiotalet env none (lift n t) in + signature_rec env c' args | _ -> []) | Const sp when args = [] && is_ml_extraction (ConstRef sp) -> [] | Const sp when is_axiom sp -> [] @@ -497,7 +499,8 @@ and signature_rec env c args = | Emlterm _ -> assert false) else let cvalue = constant_value env sp in - signature env (applist (cvalue, args)) + let c' = whd_betaiotalet env none (applist (cvalue, args)) in + signature_rec env c' [] | Ind spi -> (match extract_inductive spi with |Iml (si,_) -> |