Conjecture declare maintenant un axiome; reorganisation VernacDefinition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 10 insertions, 9 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 4290eca61..f4a8580eb 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -551,8 +551,8 @@ let solve_hook n =
 let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 
 let interp_search_about_item = function
-  | SearchRef qid -> SearchRef (Nametab.global qid)
-  | SearchString s as x -> x
+  | SearchRef qid -> GlobSearchRef (Nametab.global qid)
+  | SearchString s -> GlobSearchString s
 
 let pcoq_search s l =
   ctv_SEARCH_LIST:=[];
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 6e44f2b11..cdf83b22b 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -159,9 +159,9 @@ let make_variable_ast name typ implicits =
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition (Global, name, DefineBody ([], None,
+  VernacDefinition ((Global,Definition), name, DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
-    (fun _ _ -> ()),GDefinition)
+    (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
 
 (* This function is inspired by print_constant *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c3355b61b..9a0ecced4 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1184,8 +1184,7 @@ let xlate_thm x = CT_thm (match x with
   | Theorem -> "Theorem"
   | Remark -> "Remark"
   | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Conjecture -> "Conjecture")
+  | Fact -> "Fact")
 
 
 let xlate_defn x = CT_defn (match x with
@@ -1196,7 +1195,9 @@ let xlate_var x = CT_var (match x with
  | (Global,Definitional) -> "Parameter"
  | (Global,Logical) -> "Axiom"
  | (Local,Definitional) -> "Variable"
- | (Local,Logical) -> "Hypothesis");;
+ | (Local,Logical) -> "Hypothesis"
+ | (Global,Conjectural) -> "Conjecture"
+ | (Local,Conjectural) -> xlate_error "No local conjecture");;
 
 
 let xlate_dep =
@@ -1472,11 +1473,11 @@ let xlate_vernac =
       xlate_error "TODO: VernacStartTheoremProof"
   | VernacSuspend -> CT_suspend
   | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt))
-  | VernacDefinition (k,s,ProveBody (bl,typ),_,_) ->
+  | VernacDefinition ((k,_),s,ProveBody (bl,typ),_) ->
       if bl <> [] then xlate_error "TODO: Def bindings";
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_formula typ))
-  | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_,_) ->
+  | VernacDefinition ((kind,_),s,DefineBody(bl,red_option,c,typ_opt),_) ->
       CT_definition
 	(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
 	   cvt_optional_eval_for_definition c red_option,