aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/clear.v
AgeCommit message (Collapse)Author
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2016-10-21sections/hints: prevent Not_found in get_type_ofMatthieu Sozeau
due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared.
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-11Correction d'un bug de clearnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10552 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Report de la révision 9577 dans le trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9578 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:02:17 +0000