diff options
| -rw-r--r-- | engine/evarutil.ml | 18 | ||||
| -rw-r--r-- | engine/evarutil.mli | 17 | ||||
| -rw-r--r-- | engine/proofview.ml | 14 | ||||
| -rw-r--r-- | engine/proofview.mli | 13 | ||||
| -rw-r--r-- | proofs/goal.ml | 3 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | test-suite/ssr/bang_rewrite.v | 13 |
7 files changed, 58 insertions, 24 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index ea71be8e43..c946125d3f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' = in Evd.add_universe_constraints evd soft -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extension of those in [sigma1]. *) -let eq_constr_univs_test sigma1 sigma2 t u = +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +let eq_constr_univs_test ~evd ~extended_evd t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in let t = EConstr.Unsafe.to_constr t @@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u = in let ans = UnivProblem.eq_constr_univs_infer_with - (fun t -> kind_of_term_upto sigma1 t) - (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) fold t u sigma2 + (fun t -> kind_of_term_upto evd t) + (fun u -> kind_of_term_upto extended_evd u) + (universes extended_evd) fold t u extended_evd in match ans with None -> false | Some _ -> true diff --git a/engine/evarutil.mli b/engine/evarutil.mli index e9d579af32..7877b94582 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map -> val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extension of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool +(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of + [t] and [u] up to existential variable instantiation and + equalisable universes. The term [t] is interpreted in [evd] while + [u] is interpreted in [extended_evd]. The universe constraints in + [extended_evd] are assumed to be an extension of those in [evd]. *) +val eq_constr_univs_test : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + constr -> + constr -> + bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe diff --git a/engine/proofview.ml b/engine/proofview.ml index 8b5bd4cd80..1fbad25d46 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -849,7 +849,8 @@ let give_up = module Progress = struct - let eq_constr = Evarutil.eq_constr_univs_test + let eq_constr evd extended_evd = + Evarutil.eq_constr_univs_test ~evd ~extended_evd (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = @@ -879,10 +880,10 @@ module Progress = struct eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body (** Equality function on goals *) - let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - eq_evar_info evars1 evars2 evi1 evi2 + let goal_equal ~evd ~extended_evd evar extended_evar = + let evi = Evd.find evd evar in + let extended_evi = Evd.find extended_evd extended_evar in + eq_evar_info evd extended_evd evi extended_evi end @@ -899,7 +900,8 @@ let tclPROGRESS t = let test = quick_test || Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f) + Progress.goal_equal ~evd:initial.solution + ~extended_evd:final.solution (drop_state i) (drop_state f) end initial.comb final.comb in if not test then diff --git a/engine/proofview.mli b/engine/proofview.mli index f90f02f3e1..d6ca94e405 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -398,7 +398,18 @@ val give_up : unit tactic val tclPROGRESS : 'a tactic -> 'a tactic module Progress : sig - val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool +(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether + the [evar_info] from [evd] corresponding to [evar] is equal to that + from [extended_evd] corresponding to [extended_evar], up to + existential variable instantiation and equalisable universes. The + universe constraints in [extended_evd] are assumed to be an + extension of the universe constraints in [evd]. *) + val goal_equal : + evd:Evd.evar_map -> + extended_evd:Evd.evar_map -> + Evar.t -> + Evar.t -> + bool end (** Checks for interrupts *) diff --git a/proofs/goal.ml b/proofs/goal.ml index 888c4785df..f95a904a5f 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -91,7 +91,8 @@ module V82 = struct let weak_progress glss gls = match glss.Evd.it with - | [ g ] -> not (Proofview.Progress.goal_equal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) + | [ g ] -> not (Proofview.Progress.goal_equal ~evd:gls.Evd.sigma + ~extended_evd:glss.Evd.sigma gls.Evd.it g) | _ -> true let progress glss gls = diff --git a/tactics/equality.ml b/tactics/equality.ml index 220b9bc475..1f125a3c59 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -255,7 +255,9 @@ let tclNOTSAMEGOAL tac = Proofview.Goal.goals >>= fun gls -> let check accu gl' = gl' >>= fun gl' -> - let accu = accu || Proofview.Progress.goal_equal sigma ev (project gl') (goal gl') in + let accu = accu || Proofview.Progress.goal_equal + ~evd:sigma ~extended_evd:(project gl') ev (goal gl') + in Proofview.tclUNIT accu in Proofview.Monad.List.fold_left check false gls >>= fun has_same -> diff --git a/test-suite/ssr/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v new file mode 100644 index 0000000000..30e6d57a7a --- /dev/null +++ b/test-suite/ssr/bang_rewrite.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. + +Require Import ssreflect. + +Axiom mult@{i} : nat -> nat -> nat. +Notation "m * n" := (mult m n). + +Axiom multA : forall a b c, (a * b) * c = a * (b * c). + +(* Previously the following gave a universe error: *) + +Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)). +Proof. by rewrite !multA. Qed. |