diff options
| author | Brian Campbell | 2018-06-07 16:20:21 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | dda8dd8689ea4756c41a5bb36a123b564dfb0b12 (patch) | |
| tree | 1e0c1c4832c31d7cb41699c49cd34b4c5cb1b98e /src | |
| parent | dff33af770e6b48c0f6592bcab7c6f4b0e3d6662 (diff) | |
Coq: track add_typquant change
Diffstat (limited to 'src')
| -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 0b52155d..53571655 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1464,7 +1464,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = (* Remove some type variables in a similar fashion to merge_kids_atoms *) let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = - let typ_env = add_typquant tqs typ_env in + let typ_env = add_typquant l tqs typ_env in match typ with | Typ_aux (Typ_fn (args_ty, ret_ty, eff),l') -> let check_typ (args,used) typ = |