diff options
| author | gmelquio | 2012-09-15 17:10:37 +0000 |
|---|---|---|
| committer | gmelquio | 2012-09-15 17:10:37 +0000 |
| commit | 730e25488e0f502359ed8c2a845b97bf0245d1e7 (patch) | |
| tree | d81f83c5c825e865ceb4fda85482e609bcebb58b /Makefile.common | |
| parent | 92616b9f660eaa2640964ca1925b05d37af70c8c (diff) | |
Port rewrites of tactic documentation from branch 8.4.
This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277,
r15278, r15337. The merge did not go without troubles, but hopefully none
of the changes were lost in process.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 63d194a4b9..654a715272 100644 --- a/Makefile.common +++ b/Makefile.common @@ -120,7 +120,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-cic.v.tex RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-decl.v.tex RefMan-pro.v.tex \ + RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ Cases.v.tex Coercion.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Helm.tex Classes.v.tex ) |
