Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

6 files changed, 36 insertions, 28 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 4f4f2039..7b746396 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -248,11 +248,11 @@ Fixpoint interpret3 t fv {struct t}: R :=
 End nsatz1.
 
 Ltac equality_to_goal H x y:=
-  let h := fresh "nH" in
   (* eliminate trivial  hypotheses, but it takes time!:
+  let h := fresh "nH" in
     (assert (h:equality x y);
     [solve [cring] | clear H; clear h])
-  || *) (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
+  || *) try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
 .
 
 Ltac equalities_to_goal :=
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index 8ac952c0..013fd0ef 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -201,7 +201,8 @@ Ltac fold_field_cond req :=
 Ltac simpl_PCond FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  try apply lemma;
+  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; 
+       clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req;
   try exact I.
@@ -209,7 +210,8 @@ Ltac simpl_PCond FLD :=
 Ltac simpl_PCond_BEURK FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  apply lemma;
+  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; 
+       clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req.
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index bc05c252..1989e9b3 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1507,13 +1507,15 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   | cons a l1 => Fcons a (Fapp l1 m)
   end.
 
-Lemma fcons_correct : forall l l1,
-  PCond l (Fapp l1 nil) -> PCond l l1.
-induction l1; simpl; intros.
- trivial.
- elim PCond_fcons_inv with (1 := H); intros.
-   destruct l1; auto.
-Qed.
+ Lemma fcons_correct : forall l l1,
+  (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
+ Proof.
+ intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
+ induction l1; simpl; intros.
+  trivial.
+  elim PCond_fcons_inv with (1 := H); intros.
+  destruct l1; trivial. split; trivial. apply IHl1; trivial.
+ Qed.
 
 End Fcons_impl.
 
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d8f46098..7a4916fa 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -559,14 +559,18 @@ and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
   let obls' = Array.copy obls in
+  let set = ref Intset.empty in
   let p = match oblset with
     | None -> (fun _ -> true)
-    | Some s -> (fun i -> Intset.mem i s)
+    | Some s -> set := s;
+      (fun i -> Intset.mem i !set)
   in
   let _ =
     Array.iteri (fun i x ->
-		 if p i && solve_obligation_by_tac prg obls' i tac then
-		   decr rem)
+      if p i && solve_obligation_by_tac prg obls' i tac then
+	let deps = dependencies obls i in
+	  (set := Intset.union !set deps;
+	   decr rem))
       obls'
   in
     update_obls prg obls' !rem
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index a14eda60..165bf83d 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -23,7 +23,7 @@ let get_module_path_of_full_path path =
     (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
   with
      [] ->
-       Pp.warning ("Modules not supported: reference to "^
+       Pp.msg_warn ("Modules not supported: reference to "^
          Libnames.string_of_path path^" will be wrong");
        dirpath
    | [modul] -> modul
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 867aac71..59ade01e 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -433,46 +433,46 @@ let kind_of_constant kn =
     | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
     | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
     | DK.IsAssumption DK.Conjectural ->
-        Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
+        Pp.msg_warn "Conjecture not supported in dtd (used Declaration instead)";
         "AXIOM","Declaration"
     | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
     | DK.IsDefinition DK.Example ->
-        Pp.warning "Example not supported in dtd (used Definition instead)";
+        Pp.msg_warn "Example not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Coercion ->
-        Pp.warning "Coercion not supported in dtd (used Definition instead)";
+        Pp.msg_warn "Coercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.SubClass ->
-        Pp.warning "SubClass not supported in dtd (used Definition instead)";
+        Pp.msg_warn "SubClass not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.CanonicalStructure ->
-        Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
+        Pp.msg_warn "CanonicalStructure not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Fixpoint ->
-        Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
+        Pp.msg_warn "Fixpoint not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.CoFixpoint ->
-        Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
+        Pp.msg_warn "CoFixpoint not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Scheme ->
-        Pp.warning "Scheme not supported in dtd (used Definition instead)";
+        Pp.msg_warn "Scheme not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.StructureComponent ->
-        Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
+        Pp.msg_warn "StructureComponent not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.IdentityCoercion ->
-        Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
+        Pp.msg_warn "IdentityCoercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Instance ->
-        Pp.warning "Instance not supported in dtd (used Definition instead)";
+        Pp.msg_warn "Instance not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsDefinition DK.Method ->
-        Pp.warning "Method not supported in dtd (used Definition instead)";
+        Pp.msg_warn "Method not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
     | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
         "THEOREM",DK.string_of_theorem_kind thm
     | DK.IsProof _ ->
-        Pp.warning "Unsupported theorem kind (used Theorem instead)";
+        Pp.msg_warn "Unsupported theorem kind (used Theorem instead)";
         "THEOREM",DK.string_of_theorem_kind DK.Theorem
 ;;