diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 3c1d87c0..12908807 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1439,7 +1439,9 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in let tqs = match tqs with | TypQ_aux (TypQ_tq qs,l) -> TypQ_aux (TypQ_tq (List.filter (function - | QI_aux (QI_id kopt,_) when is_nat_kopt kopt -> KidSet.mem (kopt_kid kopt) used + | QI_aux (QI_id kopt,_) when is_nat_kopt kopt -> + let kid = kopt_kid kopt in + KidSet.mem kid used && not (KidSet.mem kid args) | _ -> true) qs),l) | _ -> tqs in @@ -1449,8 +1451,10 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = parens (doc_var_lem empty_ctxt kid ^^ string " : Z") | _ -> parens (underscore ^^ string " : " ^^ doc_typ empty_ctxt typ) in - let typs_pp = separate space (List.map doc_typ' typs) ^/^ comma ^/^ doc_typ empty_ctxt ret_ty in - string "forall" ^/^ doc_typquant_items empty_ctxt braces tqs ^/^ typs_pp + let arg_typs_pp = separate space (List.map doc_typ' typs) in + let ret_typ_pp = doc_typ empty_ctxt ret_ty in + let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in + string "forall" ^/^ tyvars_pp ^/^ arg_typs_pp ^/^ constrs_pp ^^ comma ^/^ ret_typ_pp | _ -> doc_typschm empty_ctxt true ts let doc_val_spec unimplemented (VS_aux (VS_val_spec(tys,id,_,_),ann)) = |