diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:13:23 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:13:23 +0000 |
| commit | d7be87d457fea915b0ec395e4fec986242a033c5 (patch) | |
| tree | 61c44fcc6a722731f764fb68dd956b178ff2fcf2 /plugins | |
| parent | 33a21e68fb5fad1d41bfaf03207054fddbb46ef0 (diff) | |
Extraction: restore (temporarily?) a very limited form of linear letin reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 37e5e6a61..df962773d 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -772,6 +772,8 @@ let is_atomic = function | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true | _ -> false +let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false + (*S The main simplification function. *) (* Some beta-iota reductions + simplifications. *) @@ -788,7 +790,7 @@ let rec simpl o = function if (is_atomic c) || (is_atomic e) || (let n = nb_occur_match e in - (n = 0 || (n=1 && (is_tmp id || o.opt_lin_let)))) + (n = 0 || (n=1 && (is_tmp id || is_imm_apply e || o.opt_lin_let)))) then simpl o (ast_subst c e) else |