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 /translate | |
| 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 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index e4fa125e1..b04ff3efc 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -382,6 +382,7 @@ let pr_thm_token = function | Decl_kinds.Lemma -> str"Lemma" | Decl_kinds.Fact -> str"Fact" | Decl_kinds.Remark -> str"Remark" + | Decl_kinds.Conjecture -> str"Conjecture" let pr_require_token = function | Some true -> str "Export" @@ -630,11 +631,9 @@ let rec pr_vernac = function (match bl with | [] -> mt() | _ -> error "Statements with local binders no longer supported") -(* -pr_vbinders bl ++ spc()) -*) ++ str":" ++ spc() ++ pr_type c) - | VernacEndProof (opac,o) -> (match o with + | VernacEndProof Admitted -> str"Admitted" + | VernacEndProof (Proved (opac,o)) -> (match o with | None -> if opac then str"Qed" else str"Defined" | Some (id,th) -> (match th with | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_id id |