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

13 files changed, 81 insertions, 40 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))
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 10ae3d79b..a47fb9086 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -17,6 +17,7 @@ type theorem_kind =
   | Lemma
   | Fact
   | Remark
+  | Conjecture
 
 type definitionkind =
   | LDefinition
@@ -63,6 +64,7 @@ type local_theorem_kind = LocalStatement
 type 'a mathematical_kind =
   | IsAssumption of type_as_formula_kind
   | IsDefinition
+  | IsConjecture
   | IsProof of 'a
 
 type global_kind = theorem_kind mathematical_kind
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 11d70529d..1cc9f038f 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 f9f731b31..eb1b3e466 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 16d2ba9c5..49f8b0d85 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 d86952e25..8e0088890 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
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 4f8d8b07f..7f8e74862 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -195,6 +195,11 @@ let cook_proof () =
       const_entry_opaque = true },
     strength, ts.top_hook))
 
+let current_proof_statement () = 
+  let ts = get_topstate() in
+  (get_current_proof_name (), ts.top_strength, 
+   ts.top_goal.evar_concl, ts.top_hook)
+
 (*********************************************************************)
 (*              Abort   functions                                    *)
 (*********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9585e7b3c..f4cc32a55 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -107,6 +107,7 @@ val set_xml_cook_proof : (pftreestate -> unit) -> unit
 val get_pftreestate : unit -> pftreestate
 
 (* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
+
 val get_end_tac : unit -> tactic option
 
 (* [get_goal_context n] returns the context of the [n]th subgoal of
@@ -119,6 +120,11 @@ val get_goal_context : int -> Evd.evar_map * env
 
 val get_current_goal_context : unit -> Evd.evar_map * env
 
+(* [current_proof_statement] *)
+
+val current_proof_statement :
+  unit -> identifier * goal_kind * types * declaration_hook
+
 (*s [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 78d208437..743f1337a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -80,6 +80,9 @@ let rec adjust_conclusion a cs = function
 
 (* 1| Constant definitions *)
 
+let definition_message id =
+  if_verbose message ((string_of_id id) ^ " is defined")
+
 let constant_entry_of_com (bl,com,comtypopt,opacity) =
   let sigma = Evd.empty in
   let env = Global.env() in
@@ -110,7 +113,7 @@ let declare_global_definition ident ce local =
   let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
   if local = Local then
     msg_warning (pr_id ident ++ str" is declared as a global definition");
-  if_verbose message ((string_of_id ident) ^ " is defined");
+  definition_message ident;
   ConstRef kn
 
 let declare_definition ident local bl red_option c typopt hook =
@@ -123,7 +126,7 @@ let declare_definition ident local bl red_option c typopt hook =
         let c =
           SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
         let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in
-        if_verbose message ((string_of_id ident) ^ " is defined");
+        definition_message ident;
         if Pfedit.refining () then 
           msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ 
           str" is not visible from current goals");
@@ -178,14 +181,15 @@ let non_type_eliminations =
 let declare_one_elimination ind =
   let (mib,mip) = Global.lookup_inductive ind in 
   let mindstr = string_of_id mip.mind_typename in
-  let declare na c t =
-    let kn = Declare.declare_constant (id_of_string na)
+  let declare s c t =
+    let id = id_of_string s in
+    let kn = Declare.declare_constant id
       (DefinitionEntry
         { const_entry_body = c;
           const_entry_type = t;
           const_entry_opaque = false }, 
        Decl_kinds.IsDefinition) in
-    Options.if_verbose ppnl (str na ++ str " is defined"); 
+    definition_message id;
     kn
   in
   let env = Global.env () in
@@ -655,7 +659,7 @@ let save id const kind hook =
 	(Global, ConstRef kn) in
   hook l r;
   Pfedit.delete_current_proof ();
-  if_verbose message ((string_of_id id) ^ " is defined")
+  definition_message id
 
 let save_named opacity =
   let id,(const,persistence,hook) = Pfedit.cook_proof () in
@@ -682,6 +686,15 @@ let save_anonymous_with_strength kind opacity save_ident =
   (* we consider that non opaque behaves as local for discharge *)
   save save_ident const (IsGlobal (Proof kind)) hook
 
+let admit () =
+  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+  if k <> IsGlobal (Proof Conjecture) then
+    error "Only statements declared as conjecture can be admitted";
+  let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in
+  hook Global (ConstRef kn);
+  Pfedit.delete_current_proof ();
+  assumption_message id
+
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e -> 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 525ca0f18..c12a49485 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -74,6 +74,10 @@ val save_anonymous : bool -> identifier -> unit
 
 val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
 
+(* [admit ()] aborts the current goal and save it as an assmumption *)
+
+val admit : unit -> unit
+
 (* [get_current_context ()] returns the evar context and env of the
    current open proof if any, otherwise returns the empty evar context
    and the current global env *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0cb0b54e1..6665af74c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -308,9 +308,11 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
       (str "Proof editing mode not supported in module types");
   start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
 
-let vernac_end_proof is_opaque idopt =
-  if_verbose show_script ();
-  match idopt with
+let vernac_end_proof = function
+  | Admitted -> admit ()
+  | Proved (is_opaque,idopt) ->
+    if_verbose show_script ();
+    match idopt with
     | None -> save_named is_opaque
     | Some (id,None) -> save_anonymous is_opaque id
     | Some (id,Some kind) -> save_anonymous_with_strength kind is_opaque id
@@ -1119,7 +1121,7 @@ let interp c = match c with
   | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f
   | VernacStartTheoremProof (k,id,t,top,f) ->
       vernac_start_proof k (Some id) t top f
-  | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt
+  | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,l) -> vernac_assumption stre l
   | VernacInductive (finite,l) -> vernac_inductive finite l
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index aa307203f..5f3ff5444 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -142,6 +142,10 @@ type local_decl_expr =
 
 type module_binder = identifier list * module_type_ast
 
+type proof_end =
+  | Admitted
+  | Proved of opacity_flag * (identifier * theorem_kind option) option
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -175,7 +179,7 @@ type vernac_expr =
       declaration_hook * definitionkind
   | VernacStartTheoremProof of theorem_kind * identifier *
       (local_binder list * constr_expr) * bool * declaration_hook
-  | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
+  | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list
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