diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | COMPATIBILITY | 38 | ||||
| -rw-r--r-- | engine/proofview.ml | 11 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4737.v | 9 | ||||
| -rw-r--r-- | theories/Compat/Coq84.v | 2 |
6 files changed, 55 insertions, 11 deletions
diff --git a/.gitignore b/.gitignore index 4127ac649..4f8c019f4 100644 --- a/.gitignore +++ b/.gitignore @@ -157,3 +157,4 @@ dev/myinclude /doc/refman/Reference-Manual.hoptind /doc/refman/Reference-Manual.optidx /doc/refman/Reference-Manual.optind +user-contrib diff --git a/COMPATIBILITY b/COMPATIBILITY index ab29903b9..883b8576d 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,6 +1,43 @@ Potential sources of incompatibilities between Coq V8.4 and V8.5 ---------------------------------------------------------------- +* List of typical changes to be done to adapt files from Coq 8.4 * +* to Coq 8.5 when not using compatibility option "-compat 8.4". * + +Symptom: "The reference omega was not found in the current environment". +Cause: "Require Omega" does not import the tactic "omega" any more +Possible solutions: +- use "Require Import OmegaTactic" (not compatible with 8.4) +- use "Require Import Omega" (compatible with 8.4) +- add definition "Ltac omega := Coq.omega.Omega.omega." + +Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective) +Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives +Possible solutions: +- use "dintuition" instead; it is stronger than "intuition" and works + uniformly on non standard connectives, such as n-ary conjunctions or disjunctions + (not compatible with 8.4) +- do the script differently + +Symptom: The constructor foo (in type bar) expects n arguments. +Cause: parameters must now be given in patterns +Possible solutions: +- use option "Set Asymmetric Patterns" (compatible with 8.4) +- add "_" for the parameters (not compatible with 8.4) +- turn the parameters into implicit arguments (compatible with 8.4) + +Symptom: "NPeano.Nat.foo" not existing anymore +Possible solutions: +- use "Nat.foo" instead + +Symptom: typing problems with proj1_sig or similar +Cause: coercion from sig to sigT and similar coercions have been + removed so as to make the initial state easier to understand for + beginners +Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) + +* Other detailed changes * + (see also file CHANGES) - options for *coq* compilation (see below for ocaml). @@ -30,7 +67,6 @@ Potential sources of incompatibilities between Coq V8.4 and V8.5 for more details: file CHANGES or section "Customization at launch time" of the reference manual. - - Universe Polymorphism. diff --git a/engine/proofview.ml b/engine/proofview.ml index 95e20bc25..45af16759 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -665,11 +665,12 @@ let with_shelf tac = (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) let goodmod p m = - let p' = p mod m in - (* if [n] is negative [n mod l] is negative of absolute value less - than [l], so [(n mod l)+l] is the representative of [n] in the - interval [[0,l-1]].*) - if p' < 0 then p'+m else p' + if m = 0 then 0 else + let p' = p mod m in + (* if [n] is negative [n mod l] is negative of absolute value less + than [l], so [(n mod l)+l] is the representative of [n] in the + interval [[0,l-1]].*) + if p' < 0 then p'+m else p' let cycle n = let open Proof in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5d1f77a5a..efc42aab7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -184,8 +184,7 @@ type inference_flags = { } let frozen_holes (sigma, sigma') = - let fold evk _ accu = Evar.Set.add evk accu in - Evd.fold_undefined fold sigma Evar.Set.empty + (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma) let pending_holes (sigma, sigma') = let fold evk _ accu = @@ -194,7 +193,7 @@ let pending_holes (sigma, sigma') = Evd.fold_undefined fold sigma' Evar.Set.empty let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen evk = Evar.Set.mem evk frozen in + let filter_frozen = frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) diff --git a/test-suite/bugs/closed/4737.v b/test-suite/bugs/closed/4737.v new file mode 100644 index 000000000..84ed45e45 --- /dev/null +++ b/test-suite/bugs/closed/4737.v @@ -0,0 +1,9 @@ +Goal True. +Proof. +exact I; cycle 1. +Qed. + +Goal True. +Proof. +exact I; swap 1 2. +Qed. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index e46a556a9..aa4411704 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -56,8 +56,6 @@ Tactic Notation "symmetry" := symmetry. Tactic Notation "split" := split. Tactic Notation "esplit" := esplit. -Global Set Regular Subst Tactic. - (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *) Require Coq.Numbers.Natural.Peano.NPeano. |