diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 | ||||
| -rw-r--r-- | ltac/profile_ltac.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4653.v | 3 | ||||
| -rw-r--r-- | theories/Reals/Sqrt_reg.v | 2 |
5 files changed, 7 insertions, 3 deletions
@@ -13,6 +13,7 @@ Bugfixes - #4592, #4932: notations sharing recursive patterns or sharing binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #3070: fixing "subst" in the presence of a chain of dependencies. Specification language diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5ba3c308a6..9fbff7181e 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1277,7 +1277,7 @@ Prints the profile Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. \begin{quote} -{\tt Reset Profile}. +{\tt Reset Ltac Profile}. \end{quote} Resets the profile, that is, deletes all accumulated information diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index f332e1a0d5..bea02e3dcb 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -139,7 +139,7 @@ let string_of_call ck = let s = string_of_ppcmds (match ck with - | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> diff --git a/test-suite/bugs/closed/4653.v b/test-suite/bugs/closed/4653.v new file mode 100644 index 0000000000..4514342c5e --- /dev/null +++ b/test-suite/bugs/closed/4653.v @@ -0,0 +1,3 @@ +Definition T := Type. +Module Type S. Parameter foo : let A := T in True. End S. +Module M <: S. Lemma foo (A := T) : True. Proof I. End M. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442e8..d43baee8cd 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. |