Intégration des modifs de la branche mowgli :

- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
  Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
  (nouveau fichier library/dischargedhypsmap.ml).


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

6 files changed, 17 insertions, 14 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8b47ced02f..a3e18f1509 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -35,7 +35,7 @@ open Safe_typing
 type proof_topstate = {
   top_hyps : named_context * named_context;
   top_goal : goal;
-  top_strength : bool * Libnames.strength;
+  top_strength : Decl_kinds.goal_kind;
   top_hook : declaration_hook }
 
 let proof_edits =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index beeb569592..4ddcc5c8d2 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -14,7 +14,7 @@ open Names
 open Term
 open Sign
 open Environ
-open Nametab
+open Decl_kinds
 open Proof_type
 open Tacmach
 (*i*)
@@ -67,7 +67,7 @@ val get_undo : unit -> int option
     declare the built constructions as a coercion or a setoid morphism) *)
 
 val start_proof : 
-  identifier -> bool * Libnames.strength -> named_context -> constr
+  identifier -> goal_kind -> named_context -> constr
     -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
@@ -91,12 +91,11 @@ val resume_proof : identifier -> unit
 val suspend_proof : unit -> unit
 
 (*s [cook_proof opacity] turns the current proof (assumed completed) into
-    a constant with its name, strength and possible hook (see [start_proof]);
+    a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed *)
 
 val cook_proof : unit -> 
-  identifier *
-  (Entries.definition_entry * (bool * Libnames.strength) * declaration_hook)
+  identifier * (Entries.definition_entry * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
 val set_xml_cook_proof : (pftreestate -> unit) -> unit
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a05464b00b..86ec64c76d 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -176,7 +176,7 @@ let prgl gl =
   (str"["  ++ pgl  ++ str"]"  ++ spc ())
 
 let pr_evgl gl =
-  let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in
+  let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in
   let pc = prterm gl.evar_concl in
   hov 0 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pc ++ str"]")
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 3d599cc485..e3d52c5b36 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -100,4 +100,4 @@ type closed_generic_argument =
 type 'a closed_abstract_argument_type =
     ('a,constr,raw_tactic_expr) abstract_argument_type
 
-type declaration_hook = Libnames.strength -> global_reference -> unit
+type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 6f86fbe3aa..95bf5d3a21 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -128,4 +128,4 @@ type closed_generic_argument =
 type 'a closed_abstract_argument_type =
     ('a,constr,raw_tactic_expr) abstract_argument_type
 
-type declaration_hook = Libnames.strength -> global_reference -> unit
+type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 071f14330d..16b13ac9ea 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -232,7 +232,12 @@ let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
   Their proof should be completed in order to complete the initial proof *)
 
 let extract_open_proof sigma pf =
-  let meta_cnt = ref 0 in
+  let next_meta = 
+    let meta_cnt = ref 0 in
+    let rec f () =
+      incr meta_cnt; if in_dom sigma !meta_cnt then f () else !meta_cnt
+    in f
+  in
   let open_obligations = ref [] in
   let rec proof_extractor vl = function
     | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
@@ -259,10 +264,9 @@ let extract_open_proof sigma pf =
 	       let (_,c,ty) = Sign.lookup_named id goal.evar_hyps in
 	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl	in
-        incr meta_cnt;
-	open_obligations := (!meta_cnt,abs_concl):: !open_obligations;
-	applist
-          (mkMeta !meta_cnt, List.map (fun (n,_) -> mkRel n) sorted_rels) 
+        let meta = next_meta () in
+	open_obligations := (meta,abs_concl):: !open_obligations;
+	applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) sorted_rels) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
   in