diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
| commit | 03b9147d4a2d9467a26b3337d843226f50aa5504 (patch) | |
| tree | 1b22245e245d533f9a413b2ae960959833fc0f52 /contrib/subtac/subtac_interp_fixpoint.ml | |
| parent | 0df132d1c1cd28db10b4ee664230f8043e9006b9 (diff) | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Merge commit 'upstream/8.0pl3+8.1beta.2' into 8.1
Diffstat (limited to 'contrib/subtac/subtac_interp_fixpoint.ml')
| -rw-r--r-- | contrib/subtac/subtac_interp_fixpoint.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml index 858fad1a..bb35833f 100644 --- a/contrib/subtac/subtac_interp_fixpoint.ml +++ b/contrib/subtac/subtac_interp_fixpoint.ml @@ -60,7 +60,7 @@ let pr_binder_list b = let rec rewrite_rec_calls l c = c - +(* let rewrite_fixpoint env l (f, decl) = let (id, (n, ro), bl, typ, body) = f in let body = rewrite_rec_calls l body in @@ -151,3 +151,4 @@ let rewrite_fixpoint env l (f, decl) = Ppconstr.pr_constr_expr body') in (id, (succ n, ro), bl', typ, body'), decl +*) |