From bd91698e1acdc5e579f904e3f52e40a57bd6cd13 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Oct 2003 12:37:03 +0000 Subject: Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé incomplètement prouvé comme axiome MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/xlate.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b7fbd7fc8..244b0543d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1202,7 +1202,8 @@ let xlate_thm x = CT_thm (match x with | Theorem -> "Theorem" | Remark -> "Remark" | Lemma -> "Lemma" - | Fact -> "Fact") + | Fact -> "Fact" + | Conjecture -> "Conjecture") let xlate_defn x = CT_defn (match x with @@ -1416,16 +1417,17 @@ let xlate_vernac = CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)) - | VernacEndProof (true,None) -> + | VernacEndProof (Proved (true,None)) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE) - | VernacEndProof (false,None) -> + | VernacEndProof (Proved (false,None)) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE) - | VernacEndProof (b,Some (s, Some kind)) -> + | VernacEndProof (Proved (b,Some (s, Some kind))) -> CT_save (CT_coerce_THM_to_THM_OPT (xlate_thm kind), ctf_ID_OPT_SOME (xlate_ident s)) - | VernacEndProof (b,Some (s,None)) -> + | VernacEndProof (Proved (b,Some (s,None))) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctf_ID_OPT_SOME (xlate_ident s)) + | VernacEndProof Admitted -> xlate_error "TODO: Admitted" | VernacSetOpacity (false, id :: idl) -> CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id, List.map loc_qualid_to_ct_ID idl)) -- cgit v1.2.3