Merge branch 'v8.5' into v8.6

9 files changed, 87 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index c25649823..8e9bcaba6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -101,6 +101,12 @@ Other bugfixes
 - #4818: "Admitted" fails due to undefined universe anomaly after calling
   "destruct"
 - #4823: remote counter: avoid thread race on sockets
+- #4841: -verbose flag changed semantics in 8.5, is much harder to use
+- #4851: [nsatz] cannot handle duplicated hypotheses
+- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant
+  of nsatz
+- #4880: [nsatz_compute] generates invalid certificates if given redundant
+  hypotheses
 - #4881: synchronizing "Declare Implicit Tactic" with backtrack.
 - #4882: anomaly with Declare Implicit Tactic on hole of type with evars
 - Fix use of "Declare Implicit Tactic" in refine.
diff --git a/COPYRIGHT b/COPYRIGHT
index 8c08e05e6..fc4b7baa4 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -1,6 +1,6 @@
                      The Coq proof assistant
 
-Copyright 1999-2015 The Coq development team, INRIA, CNRS, University
+Copyright 1999-2016 The Coq development team, INRIA, CNRS, University
 Paris Sud, University Paris 7, Ecole Polytechnique.
 
 This product includes also software developed by
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 93dad18d9..36bce780b 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -468,6 +468,44 @@ let theoremedeszeros lpol p =
 
 open Ideal
 
+(* Remove zero polynomials and duplicates from the list of polynomials lp
+   Return (clp, lb)
+   where clp is the reduced list and lb is a list of booleans
+   that has the same size than lp and where true indicates an
+   element that has been removed
+ *)
+let rec clean_pol lp =
+  let t = Hashpol.create 12 in
+  let find p = try Hashpol.find t p 
+               with 
+                 Not_found -> Hashpol.add t p true; false in
+  let rec aux lp =
+    match lp with
+    | [] -> [], []
+    | p :: lp1 -> 
+      let clp, lb = aux lp1 in
+      if equal p zeroP ||  find p then clp, true::lb 
+       else
+        (p :: clp, false::lb) in
+     aux lp
+
+(* Expand the list of polynomials lp putting zeros where the list of 
+   booleans lb indicates there is a missing element 
+   Warning:
+   the expansion is relative to the end of the list in reversed order
+   lp cannot have less elements than lb
+*)
+let expand_pol lb lp =
+ let rec aux lb lp = 
+   match lb with
+   | [] -> lp
+   | true :: lb1 ->  zeroP :: aux lb1 lp
+   | false :: lb1 ->
+     match lp with
+     [] -> assert false
+     | p :: lp1 -> p :: aux lb1 lp1 
+  in List.rev (aux lb (List.rev lp))
+
 let theoremedeszeros_termes lp =
   nvars:=0;(* mise a jour par term_pol_sparse *)
   List.iter set_nvars_term  lp;
@@ -518,20 +556,29 @@ let theoremedeszeros_termes lp =
       | [] -> assert false
       | p::lp1 ->
 	  let lpol = List.rev lp1 in
+          (* preprocessing :
+             we remove zero polynomials and duplicate that are not handled by in_ideal
+             lb is kept in order to fix the certificate in the post-processing 
+          *)
+	  let lpol, lb  = clean_pol lpol in
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
           info "cert ok\n";
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
 	  match remove_zeros (fun x -> equal x zeroP) lc with
 	  | [] -> assert false
 	  | (lq::lci) ->
+              (* post-processing : we apply the correction for the last line *)
+              let lq = expand_pol lb lq in
 	      (* lci commence par les nouveaux polynomes *)
-	      let m= !nvars in
+	      let m = !nvars in
 	      let c = pol_sparse_to_term m (polconst m cert.coef) in
 	      let r = Pow(Zero,cert.power) in
 	      let lci = List.rev lci in
+              (* post-processing we apply the correction for the other lines *)
+	      let lci = List.map (expand_pol lb) lci in
 	      let lci = List.map (List.map (pol_sparse_to_term m)) lci in
 	      let lq = List.map (pol_sparse_to_term m) lq in
-	      info ("number of parametres: "^string_of_int nparam^"\n");
+	      info ("number of parameters: "^string_of_int nparam^"\n");
 	      info "term computed\n";
 	      (c,r,lci,lq)
       )
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 58b881174..5f0cc73d2 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -56,6 +56,6 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"", str "Instance is not well-typed in the environment of " ++
-                 str (string_of_existential evk))
+                 pr_existential_key sigma evk ++ str ".")
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v
new file mode 100644
index 000000000..a2fa93832
--- /dev/null
+++ b/test-suite/bugs/closed/4858.v
@@ -0,0 +1,7 @@
+Require Import Nsatz.
+Goal True.
+try nsatz_compute
+ (PEc 0%Z :: PEc (-1)%Z
+    :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1
+       :: PEsub (PEX Z 1) (PEX Z 1) :: nil).
+Abort.
diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v
new file mode 100644
index 000000000..5569798d5
--- /dev/null
+++ b/test-suite/bugs/closed/4880.v
@@ -0,0 +1,11 @@
+Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.
+Local Open Scope R.
+
+Goal forall x y : R,
+  x*x =  y *  y ->
+  x*x = -y * -y ->
+  x*(x*x) = 0 -> (* The associativity does not actually matter, *)
+  (x*x)*x = 0.   (* just otherwise [assumption] would solve the goal. *)
+Proof.
+  nsatz.
+Qed.
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 75dd38fde..8e5708cf0 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 6354ad469..62e9ef4b2 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -5,3 +5,6 @@ Unable to unify "nat" with "True".
 The command has indeed failed with message:
 In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
+The command has indeed failed with message:
+Ltac call to "instantiate" failed.
+Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 352c87385..424d24801 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -16,3 +16,12 @@ Goal True.
 Fail simpl; apply 0.
 Fail simpl; f 0.
 Abort.
+
+(* Test instantiate error messages *)
+
+Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
+intros T1 P1 H1.
+eexists ?[x].
+destruct H1 as [x1 H1].
+Fail instantiate (x:=projT1 x1).
+Abort.