diff options
| author | Brian Campbell | 2018-12-18 10:30:27 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-12-19 17:55:26 +0000 |
| commit | 66b55de7e24ab546aff3eba17d21b86d47306a6d (patch) | |
| tree | 55accf59fb23bf7d275b1191391560411f763d9b /src | |
| parent | 07a332c856b3ee9fe26a9cd47ea6005f9d579810 (diff) | |
Coq: handle existentials in hypotheses during solving, add max_nat, better casts
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 18e288dd..4f6a0dfc 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1383,7 +1383,11 @@ let doc_exp, doc_let = if effects then if inner_ex then if cast_ex - then string "derive_m" ^^ space ^^ epp + (* If the types are the same use the cast as a hint to Coq, + otherwise derive the new type from the old one. *) + then if alpha_equivalent env inner_typ cast_typ + then epp + else string "derive_m" ^^ space ^^ epp else string "projT1_m" ^^ space ^^ epp else if cast_ex then string "build_ex_m" ^^ space ^^ epp |