diff options
-rw-r--r-- | CHANGES | 6 | ||||
-rw-r--r-- | COPYRIGHT | 2 | ||||
-rw-r--r-- | plugins/nsatz/nsatz.ml | 51 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4858.v | 7 | ||||
-rw-r--r-- | test-suite/bugs/closed/4880.v | 11 | ||||
-rw-r--r-- | test-suite/csdp.cache | bin | 79491 -> 79491 bytes | |||
-rw-r--r-- | test-suite/output/Errors.out | 3 | ||||
-rw-r--r-- | test-suite/output/Errors.v | 9 |
9 files changed, 87 insertions, 4 deletions
@@ -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. @@ -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 Binary files differindex 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. |