From e1e0eaeb16dd1fcf3067a9695cb2c6d7bba292bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 4 Apr 2024 11:50:38 +0200 Subject: [PATCH] coq: export (opaque) definition as (opaque) Definition instead of as Lemma --- src/export/coq.ml | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/export/coq.ml b/src/export/coq.ml index eff11fa5a..c32b72240 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -278,9 +278,6 @@ and typopt : p_term option pp = fun ppf t -> Option.iter (out ppf " : %a" term) t (** Translation of commands. *) - -let is_lem x = is_opaq x || is_priv x - let command : p_command pp = fun ppf {elt; pos} -> begin match elt with | P_inductive _ -> wrn pos "TODO"; assert false @@ -304,13 +301,10 @@ let command : p_command pp = fun ppf {elt; pos} -> in begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with | true, Some t, _, _ -> - if List.exists is_lem p_sym_mod then - out ppf "Lemma %a%a%a.\nProof. exact (%a). Qed.@." - ident p_sym_nam params_list p_sym_arg typopt p_sym_typ - term t - else - out ppf "Definition %a%a := %a.@." - ident p_sym_nam params_list p_sym_arg term t + out ppf "Definition %a%a%a := %a.@." + ident p_sym_nam params_list p_sym_arg typopt p_sym_typ term t; + if List.exists is_opaq p_sym_mod then + out ppf "Opaque %a.@." ident p_sym_nam | false, _, [], Some t -> out ppf "Axiom %a : %a.@." ident p_sym_nam term t | false, _, _, Some t ->