diff options
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 = |