diff options
27 files changed, 143 insertions, 132 deletions
@@ -57,6 +57,9 @@ Tactics - A bug fixed in "rewrite H in *" and "rewrite H in * |-" may cause a few rare incompatibilities (it was unintendedly recursively rewriting in the side conditions generated by H). +- Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure + properties of the executation of a tactic without keeping the effect + of the execution. Focusing diff --git a/Makefile.build b/Makefile.build index f583c3337..ffe605757 100644 --- a/Makefile.build +++ b/Makefile.build @@ -386,21 +386,16 @@ coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) -COQTOP_OPT_MLTOP=toplevel/coqtop_opt_bin.cmx -COQTOP_BYTE_MLTOP=toplevel/coqtop_byte_bin.cmo - -$(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< +COQTOP_OPT=toplevel/coqtop_opt_bin.ml +COQTOP_BYTE=toplevel/coqtop_byte_bin.ml ifeq ($(BEST),opt) -$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) +$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun \ - $(SYSMOD) -package camlp5.gramlib \ - $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ - $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $(COQTOP_OPT) -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -409,13 +404,12 @@ $(COQTOPEXE): $(COQTOPBYTE) endif # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM -$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ + $(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ - $(LINKCMO) $(BYTEFLAGS) \ - $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ + $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@ # For coqc COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 0a4d0ef9a..3ed697d8b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -156,6 +156,8 @@ is understood as & | & {\tt type\_term} {\term}\\ & | & {\tt numgoals} \\ & | & {\tt guard} {\it test}\\ +& | & {\tt assert\_fails} {\tacexprpref}\\ +& | & {\tt assert\_succeds} {\tacexprpref}\\ & | & \atomictac\\ & | & {\qualid} \nelist{\tacarg}{}\\ & | & {\atom} @@ -598,6 +600,22 @@ The experimental status of this tactic pertains to the fact if $v$ performs side \ErrMsg \errindex{This tactic has more than one success} +\subsubsection[Checking the failure]{Checking the failure\tacindex{assert\_fails}\index{Tacticals!assert\_fails@{\tt assert\_fails}}} + +Coq provides a derived tactic to check that a tactic \emph{fails}: +\begin{quote} +{\tt assert\_fails} {\tacexpr} +\end{quote} +This behaves like {\tt tryif {\tacexpr} then fail 0 tac "succeeds" else idtac}. + +\subsubsection[Checking the success]{Checking the success\tacindex{assert\_succeeds}\index{Tacticals!assert\_succeeds@{\tt assert\_succeeds}}} + +Coq provides a derived tactic to check that a tactic has \emph{at least one} success: +\begin{quote} +{\tt assert\_succeeds} {\tacexpr} +\end{quote} +This behaves like {\tt tryif (assert\_fails tac) then fail 0 tac "fails" else idtac}. + \subsubsection[Solving]{Solving\tacindex{solve} \index{Tacticals!solve@{\tt solve}}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 40ba43b6c..2597e3c37 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3505,17 +3505,6 @@ reduced to \texttt{S t}. \end{Variants} \begin{quote} -\optindex{Refolding Reduction} -{\tt Refolding Reduction} -\end{quote} -\emph{Deprecated since 8.7} - -This option (off by default) controls the use of the refolding strategy -of {\tt cbn} while doing reductions in unification, type inference and -tactic applications. It can result in expensive unifications, as -refolding currently uses a potentially exponential heuristic. - -\begin{quote} \optindex{Debug RAKAM} {\tt Set Debug RAKAM} \end{quote} diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e8b19f6bc..44a69d1c1 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,19 +29,6 @@ exception Elimconst their parameters in its stack. *) -let refolding_in_reduction = ref false -let _ = Goptions.declare_bool_option { - Goptions.optdepr = true; (* remove in 8.8 *) - Goptions.optname = - "Perform refolding of fixpoints/constants like cbn during reductions"; - Goptions.optkey = ["Refolding";"Reduction"]; - Goptions.optread = (fun () -> !refolding_in_reduction); - Goptions.optwrite = (fun a -> refolding_in_reduction:=a); -} - -let get_refolding_in_reduction () = !refolding_in_reduction -let set_refolding_in_reduction = (:=) refolding_in_reduction - (** Support for reduction effects *) open Mod_subst @@ -1135,7 +1122,7 @@ let local_whd_state_gen flags sigma = whrec let raw_whd_state_gen flags env = - let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ()) + let f sigma s = fst (whd_state_gen ~refold:false ~tactic_mode:false flags env sigma s) in f @@ -1561,7 +1548,7 @@ let is_sort env sigma t = of case/fix (heuristic used by evar_conv) *) let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = - let refold = get_refolding_in_reduction () in + let refold = false in let tactic_mode = false in let rec whrec csts s = let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 3b56513f5..29dc3ed0f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -31,11 +31,6 @@ module ReductionBehaviour : sig val print : Globnames.global_reference -> Pp.t end -(** Option telling if reduction should use the refolding machinery of cbn - (off by default) *) -val get_refolding_in_reduction : unit -> bool -val set_refolding_in_reduction : bool -> unit - (** {6 Support for reduction effects } *) type effect_name = string diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/opened/3424.v index ee8cabf17..d1c5bb68f 100644 --- a/test-suite/bugs/closed/3424.v +++ b/test-suite/bugs/opened/3424.v @@ -13,12 +13,12 @@ Notation "0" := (trunc_S minus_one) : trunc_scope. Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Notation IsHProp := (IsTrunc minus_one). Notation IsHSet := (IsTrunc 0). -Set Refolding Reduction. Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. Proof. intros. eexists. (* exact (H' a b). *) (* Undo. *) -apply (H' a b). +Fail apply (H' a b). +exact (H' a b). Qed. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index abf8be72e..d163dfbcd 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -40,7 +40,7 @@ Proof. Qed. -Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z. +Lemma QdenZpower : forall x : Q, Zpos (Qden (x ^ 2)%Q) = (Zpos (Qden x) ^ 2) %Z. Proof. intros. destruct x. @@ -54,9 +54,9 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). - apply integer_statement; exists (Qnum x); exists (' Qden x); auto. + apply integer_statement; exists (Qnum x); exists (Zpos (Qden x)); auto. Qed. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 668b4e578..6f41b2fcf 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -149,24 +149,24 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i} -(* i Top.41 Top.42 |= *) +axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i} +(* i Top.44 Top.45 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i} -(* i Top.41 Top.42 |= *) +axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i} +(* i Top.44 Top.45 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.44} -> Type@{axbar'.i} +axfoo' : Type@{Top.47} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.44} -> Type@{axbar'.i} +axbar' : Type@{Top.47} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 266d94ad9..c6efc240a 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -44,6 +44,9 @@ Module mono. Monomorphic Definition monomono := Type@{MONOU}. Check monomono. + + Monomorphic Inductive monoind@{i} : Type@{i} := . + Monomorphic Record monorecord@{i} : Type@{i} := mkmonorecord {}. End mono. Check mono.monomono. (* qualified MONOU *) Import mono. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 5e9eff048..f7ffd1959 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -4,8 +4,6 @@ fun e : option L => match e with | None => None end : option L -> option L -fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H - : forall m n p : nat, S m <= S n + p -> m <= n + p fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 73169dae6..57a4739e9 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -13,12 +13,6 @@ Definition P (e:option L) := Print P. -(* Check that plus is folded even if reduction is involved *) -Set Warnings Append "-deprecated-option". -Set Refolding Reduction. -Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). - - (* Check that the heuristic to solve constraints is not artificially dependent on the presence of a let-in, and in particular that the second [_] below is not inferred to be n, as if obtained by diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 9e6c26b10..8df533e74 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -255,6 +255,7 @@ Tactic Notation "dependent" "induction" ident(H) := writing a version of [inversion] / [dependent destruction] which does not lose information, i.e., does not turn a goal which is provable into one which requires axiom K / UIP. *) + Ltac simpl_proj_exist_in H := repeat match type of H with | context G[proj1_sig (exist _ ?x ?p)] @@ -310,8 +311,20 @@ Ltac inversion_sigma_step := Ltac inversion_sigma := repeat inversion_sigma_step. (** A version of [time] that works for constrs *) + Ltac time_constr tac := let eval_early := match goal with _ => restart_timer end in let ret := tac () in let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in ret. + +(** Useful combinators *) + +Ltac assert_fails tac := + tryif tac then fail 0 tac "succeeds" else idtac. +Ltac assert_succeeds tac := + tryif (assert_fails tac) then fail 0 tac "fails" else idtac. +Tactic Notation "assert_succeeds" tactic3(tac) := + assert_succeeds tac. +Tactic Notation "assert_fails" tactic3(tac) := + assert_fails tac. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 467f263be..35706e7fa 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -227,9 +227,7 @@ Infix "/" := Qdiv : Q_scope. (** A light notation for [Zpos] *) -Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. - -Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b). +Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b). Proof. unfold Qeq. simpl. ring. Qed. @@ -242,9 +240,9 @@ Proof. Open Scope Z_scope. intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. simpl_mult; ring_simplify. - replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring. + replace (p1 * Zpos r2 * Zpos q2) with (p1 * Zpos q2 * Zpos r2) by ring. rewrite H. - replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring. + replace (r1 * Zpos p2 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * Zpos p2 * Zpos q2) by ring. rewrite H0. ring. Close Scope Z_scope. @@ -255,7 +253,7 @@ Proof. unfold Qeq, Qopp; simpl. Open Scope Z_scope. intros x y H; simpl. - replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring. + replace (- Qnum x * Zpos (Qden y)) with (- (Qnum x * Zpos (Qden y))) by ring. rewrite H; ring. Close Scope Z_scope. Qed. @@ -272,9 +270,9 @@ Proof. Open Scope Z_scope. intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. intros; simpl_mult; ring_simplify. - replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring. + replace (q1 * s1 * Zpos p2) with (q1 * Zpos p2 * s1) by ring. rewrite <- H. - replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring. + replace (p1 * r1 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * p1 * Zpos q2) by ring. rewrite H0. ring. Close Scope Z_scope. @@ -305,13 +303,13 @@ Proof. unfold Qeq, Qcompare. Open Scope Z_scope. intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *. - rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)). - rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)). - change ('(q2*s2)) with ('q2 * 's2). - change ('(p2*r2)) with ('p2 * 'r2). - replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring. + rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)). + rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)). + change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2). + change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2). + replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring. rewrite H. - replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring. + replace (Zpos q2 * Zpos s2 * (r1*Zpos p2)) with ((r1*Zpos s2)*Zpos q2*Zpos p2) by ring. rewrite H'. f_equal; ring. Close Scope Z_scope. @@ -572,8 +570,8 @@ Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Z.mul_le_mono_pos_r with ('y2); [easy|]. - apply Z.le_trans with (y1 * 'x2 * 'z2). + apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|]. + apply Z.le_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_le_mono_pos_r. @@ -620,8 +618,8 @@ Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Z.mul_lt_mono_pos_r with ('y2); [easy|]. - apply Z.le_lt_trans with (y1 * 'x2 * 'z2). + apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|]. + apply Z.le_lt_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_lt_mono_pos_r. @@ -632,8 +630,8 @@ Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z. Proof. unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Z.mul_lt_mono_pos_r with ('y2); [easy|]. - apply Z.lt_le_trans with (y1 * 'x2 * 'z2). + apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|]. + apply Z.lt_le_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_le_mono_pos_r. @@ -723,9 +721,9 @@ Proof. match goal with |- ?a <= ?b => ring_simplify a b end. rewrite Z.add_comm. apply Z.add_le_mono. - match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. auto with zarith. - match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. auto with zarith. Close Scope Z_scope. Qed. @@ -740,9 +738,9 @@ Proof. match goal with |- ?a < ?b => ring_simplify a b end. rewrite Z.add_comm. apply Z.add_le_lt_mono. - match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. auto with zarith. - match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. do 2 (apply Z.mul_lt_mono_pos_r;try easy). Close Scope Z_scope. Qed. diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 48be89417..31eb41bc9 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -28,8 +28,8 @@ intros [xn xd] [yn yd] H. simpl. unfold Qeq in *. simpl in *. -change (' yd)%Z with (Z.abs (' yd)). -change (' xd)%Z with (Z.abs (' xd)). +change (Zpos yd)%Z with (Z.abs (Zpos yd)). +change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. congruence. Qed. @@ -88,8 +88,8 @@ unfold Qplus. unfold Qle. simpl. apply Z.mul_le_mono_nonneg_r;auto with *. -change (' yd)%Z with (Z.abs (' yd)). -change (' xd)%Z with (Z.abs (' xd)). +change (Zpos yd)%Z with (Z.abs (Zpos yd)). +change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. apply Z.abs_triangle. Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index e25f69c31..1510a7b82 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -30,7 +30,7 @@ Lemma Qred_identity : Proof. intros (a,b) H; simpl in *. rewrite <- Z.ggcd_gcd in H. - generalize (Z.ggcd_correct_divisors a ('b)). + generalize (Z.ggcd_correct_divisors a (Zpos b)). destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst. rewrite !Z.mul_1_l. now intros (<-,<-). Qed. @@ -39,7 +39,7 @@ Lemma Qred_identity2 : forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. intros (a,b) H; simpl in *. - generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. injection H as <- <-. intros H (_,H'). diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 3fd78f092..010782209 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -90,7 +90,7 @@ rewrite Qinv_power. reflexivity. Qed. -Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. +Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z (Zpos p))^n. Proof. intros n p. rewrite Qmake_Qdiv. @@ -190,7 +190,7 @@ unfold Z.succ. rewrite Zpower_exp; auto with *; try discriminate. rewrite Qpower_plus' by discriminate. rewrite <- IHn by discriminate. -replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring. +replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring. ring_simplify. reflexivity. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 14ab1700e..c83296259 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -167,8 +167,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. intros; field; auto. intros; - change (IZR (Zneg x2)) with (- IZR (' x2))%R; - change (IZR (Zneg p)) with (- IZR (' p))%R; + change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R; + change (IZR (Zneg p)) with (- IZR (Zpos p))%R; simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 7b08515d2..17307c827 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -21,14 +21,14 @@ Notation Z2P_correct := Z2Pos.id (only parsing). Definition Qred (q:Q) := let (q1,q2) := q in - let (r1,r2) := snd (Z.ggcd q1 ('q2)) + let (r1,r2) := snd (Z.ggcd q1 (Zpos q2)) in r1#(Z.to_pos r2). Lemma Qred_correct : forall q, (Qred q) == q. Proof. unfold Qred, Qeq; intros (n,d); simpl. - generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d)) - (Z.ggcd_correct_divisors n ('d)). + generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d)) + (Z.ggcd_correct_divisors n (Zpos d)). destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl. Open Scope Z_scope. intros Hg LE (Hn,Hd). rewrite Hd, Hn. @@ -45,13 +45,13 @@ Proof. unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. intros H. - generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) - (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b)) + (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). simpl. intros <- Hg1 Hg2 (Hg3,Hg4). assert (Hg0 : g <> 0) by (intro; now subst g). - generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) - (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). + generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d)) + (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). assert (Hg'0 : g' <> 0) by (intro; now subst g'). diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index e4e974972..7c5ddbb6a 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -80,11 +80,11 @@ unfold Qlt. simpl. replace (n*1)%Z with n by ring. ring_simplify. -replace (n / ' d * ' d + ' d)%Z with - (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring. +replace (n / Zpos d * Zpos d + Zpos d)%Z with + ((Zpos d * (n / Zpos d) + n mod Zpos d) + Zpos d - n mod Zpos d)%Z by ring. rewrite <- Z_div_mod_eq; auto with*. rewrite <- Z.lt_add_lt_sub_r. -destruct (Z_mod_lt n ('d)); auto with *. +destruct (Z_mod_lt n (Zpos d)); auto with *. Qed. Hint Resolve Qlt_floor : qarith. @@ -107,9 +107,9 @@ Proof. intros [xn xd] [yn yd] Hxy. unfold Qle in *. simpl in *. -rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *. -rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *. -rewrite (Z.mul_comm ('yd) ('xd)). +rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *. +rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *. +rewrite (Z.mul_comm (Zpos yd) (Zpos xd)). apply Z_div_le; auto with *. Qed. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 341888d09..cd831c05c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -344,13 +344,13 @@ let init_color color_mode = match colors with | None -> (** Default colors *) + Topfmt.default_styles (); Topfmt.init_terminal_output ~color:true | Some "" -> (** No color output *) Topfmt.init_terminal_output ~color:false | Some s -> (** Overwrite all colors *) - Topfmt.clear_styles (); Topfmt.parse_color_config s; Topfmt.init_terminal_output ~color:true end diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml deleted file mode 100644 index 56aced92a..000000000 --- a/toplevel/coqtop_bin.ml +++ /dev/null @@ -1,2 +0,0 @@ -(* Main coqtop initialization *) -let () = Coqtop.start() diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml index 7d8354ec3..0b65cebbb 100644 --- a/toplevel/coqtop_byte_bin.ml +++ b/toplevel/coqtop_byte_bin.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = begin try (* Enable rectypes in the toplevel if it has the directive #rectypes *) @@ -18,4 +28,7 @@ let drop_setup () = ml_loop = (fun () -> Toploop.loop ppf); }) -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml index 410b4679a..ea4c0ea52 100644 --- a/toplevel/coqtop_opt_bin.ml +++ b/toplevel/coqtop_opt_bin.ml @@ -1,3 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = Mltop.remove () -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() diff --git a/vernac/record.ml b/vernac/record.ml index e21f53f55..6e745b2af 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -594,13 +594,12 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in - let gr = match kind with + match kind with | Class def -> - let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities in - gr - | _ -> + let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in + declare_class finite def cum pl univs (loc,idstruc) idbuild + implpars params arity template implfs fields is_coe coers priorities + | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs @@ -618,7 +617,4 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in - IndRef ind - in - Declare.declare_univ_binders gr pl; - gr + IndRef ind diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 4e4077f42..055f6676e 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -187,8 +187,8 @@ let init_tag_map styles = let set accu (name, st) = CString.Map.add name st accu in tag_map := List.fold_left set !tag_map styles -let clear_styles () = - tag_map := CString.Map.empty +let default_styles () = + init_tag_map (default_tag_map ()) let parse_color_config file = let styles = Terminal.parse file in @@ -257,7 +257,6 @@ let make_printing_functions () = print_prefix, print_suffix let init_terminal_output ~color = - init_tag_map (default_tag_map ()); let push_tag, pop_tag, clear_tag = make_style_stack () in let print_prefix, print_suffix = make_printing_functions () in let tag_handler ft = { diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 2fdefc6fc..579b456a2 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -43,7 +43,7 @@ val std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit (** Color output *) -val clear_styles : unit -> unit +val default_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list |