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

4 files changed, 24 insertions, 20 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 11d70529d7..1cc9f038fd 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -36,23 +36,21 @@ GEXTEND Gram
   ;
   command:
     [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c
-(*VernacGoal c*)
-(*      | IDENT "Goal" -> VernacGoal None*)
       | "Proof" -> VernacProof Tacexpr.TacId
       | "Proof"; "with"; ta = tactic -> VernacProof ta
-(* Used ?? 
-      |	IDENT "Begin" -> VernacNop
-*)
       | IDENT "Abort" -> VernacAbort None
       | IDENT "Abort"; IDENT "All" -> VernacAbortAll
       | IDENT "Abort"; id = identref -> VernacAbort (Some id)
-      | "Qed" -> VernacEndProof (true,None)
-      | IDENT "Save" -> VernacEndProof (true,None)
-      | IDENT "Defined" -> VernacEndProof (false,None)
-      |	IDENT "Defined"; id=base_ident -> VernacEndProof (false,Some (id,None))
+      | IDENT "Admitted" -> VernacEndProof Admitted
+      | "Qed" -> VernacEndProof (Proved (true,None))
+      | IDENT "Save" -> VernacEndProof (Proved (true,None))
+      | IDENT "Defined" -> VernacEndProof (Proved (false,None))
+      |	IDENT "Defined"; id=base_ident -> 
+	  VernacEndProof (Proved (false,Some (id,None)))
       | IDENT "Save"; tok = thm_token; id = base_ident ->
-	  VernacEndProof (true,Some (id,Some tok))
-      | IDENT "Save"; id = base_ident -> VernacEndProof (true,Some (id,None))
+	  VernacEndProof (Proved (true,Some (id,Some tok)))
+      | IDENT "Save"; id = base_ident ->
+	  VernacEndProof (Proved (true,Some (id,None)))
       | IDENT "Suspend" -> VernacSuspend
       | IDENT "Resume" -> VernacResume None
       | IDENT "Resume"; id = identref -> VernacResume (Some id)
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index f9f731b319..eb1b3e4661 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -43,13 +43,16 @@ GEXTEND Gram
       | IDENT "Abort"; id = identref -> VernacAbort (Some id)
       | IDENT "Existential"; n = natural; c = constr_body ->
 	  VernacSolveExistential (n,c)
-      | IDENT "Qed" -> VernacEndProof (true,None)
-      | IDENT "Save" -> VernacEndProof (true,None)
+      | IDENT "Admitted" -> VernacEndProof Admitted
+      | IDENT "Qed" -> VernacEndProof (Proved (true,None))
+      | IDENT "Save" -> VernacEndProof (Proved (true,None))
       | IDENT "Save"; tok = thm_token; id = base_ident ->
-	  VernacEndProof (true,Some (id,Some tok))
-      | IDENT "Save"; id = base_ident -> VernacEndProof (true,Some (id,None))
-      | IDENT "Defined" -> VernacEndProof (false,None)
-      |	IDENT "Defined"; id=base_ident -> VernacEndProof (false,Some (id,None))
+	  VernacEndProof (Proved (true,Some (id,Some tok)))
+      | IDENT "Save"; id = base_ident ->
+	  VernacEndProof (Proved (true,Some (id,None)))
+      | IDENT "Defined" -> VernacEndProof (Proved (false,None))
+      |	IDENT "Defined"; id=base_ident -> 
+	  VernacEndProof (Proved (false,Some (id,None)))
       | IDENT "Suspend" -> VernacSuspend
       | IDENT "Resume" -> VernacResume None
       | IDENT "Resume"; id = identref -> VernacResume (Some id)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 16d2ba9c57..49f8b0d85b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -108,7 +108,8 @@ GEXTEND Gram
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
       | IDENT "Fact" -> Fact
-      | IDENT "Remark" -> Remark ] ]
+      | IDENT "Remark" -> Remark
+      | IDENT "Conjecture" -> Conjecture ] ]
   ;
   def_token:
     [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index d86952e25d..8e00888905 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -63,7 +63,8 @@ GEXTEND Gram
   ;
   subgoal_command:
     [ [ c = check_command; "." -> c
-      | tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] ->
+      | tac = Tactic.tactic;
+        use_dft_tac = [ "." -> false | [ "..." | ".."; "." ] -> true ] ->
           (fun g ->
             let g = match g with Some gl -> gl | _ -> 1 in
             VernacSolve(g,tac,use_dft_tac)) ] ]
@@ -135,7 +136,8 @@ GEXTEND Gram
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
       | IDENT "Fact" -> Fact
-      | IDENT "Remark" -> Remark ] ]
+      | IDENT "Remark" -> Remark
+      | IDENT "Conjecture" -> Conjecture ] ]
   ;
   def_token:
     [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition