Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

Commit 63d61d3b authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

No longer use "Implicit Arguments" now that support for Coq 8.4 has been dropped.

parent 5f91ebcb
......@@ -313,7 +313,6 @@ Qed.
Definition wgt (k:(nat * Z)%type) := match k with
| (_, p) => p
end.
Implicit Arguments wgt.
Goal wgt (S O, 3) = 3.
ae.
......
......@@ -687,8 +687,8 @@ let print_data_whytype_and_implicits info fmt (name,ts,csl) =
let _, _, all_ty_params = ls_ty_vars cs in
if not (Stv.is_empty all_ty_params) then
let print fmt tv =
fprintf fmt "[%a]" (print_tv info ~whytypes:false) tv in
fprintf fmt "@[<2>Implicit Arguments %a@ [%a].@]@\n"
fprintf fmt "{%a}" (print_tv info ~whytypes:false) tv in
fprintf fmt "@[<2>Arguments %a@ %a.@]@\n"
print_ls cs
(print_list space print) ts.ts_args)
csl;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment