diff options
| author | Brian Campbell | 2018-12-29 14:59:09 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-12-29 14:59:09 +0000 |
| commit | 771f041a48f611a4869a7a19fa39672581b5ba9a (patch) | |
| tree | 9d1f45ab16c09682a4394dd32e77e87d4fb5dcbe /src/pretty_print_coq.ml | |
| parent | ac945514d59d91e51a63149b39b472421e59e299 (diff) | |
Coq: ensure that recursive functions compute
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 09c6cafc..08844eb5 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1296,7 +1296,7 @@ let doc_exp, doc_let = [parens (string "_limit_reduces _acc")] else match f with | Id_aux (Id x,_) when is_prefix "#rec#" x -> - main_call @ [parens (string "Zwf_well_founded _ _")] + main_call @ [parens (string "Zwf_guarded _")] | _ -> main_call in hang 2 (flow (break 1) all) in |