diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 12:37:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 12:37:03 +0000 |
| commit | bd91698e1acdc5e579f904e3f52e40a57bd6cd13 (patch) | |
| tree | 0618b73cba5e1321ec6f1236f803e8c74cccf48b /contrib/interface/xlate.ml | |
| parent | f844897e7258db969e86f2e48e50e29ca5ec5802 (diff) | |
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé incomplètement prouvé comme axiome
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 12 |
1 files changed, 7 insertions, 5 deletions
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)) |