aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcorbinea2003-11-26 14:34:47 +0000
committercorbinea2003-11-26 14:34:47 +0000
commit60851fb12869ef3ca85b56a6d4bd2f57f33af517 (patch)
treee504afc15688a2cf4caadd6728b9a1bac53d43f8
parentcdb1422b199d1966fb2276c197a3d2ed516a735f (diff)
just forgot something in previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4995 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/cc/CC.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/cc/CC.v b/contrib/cc/CC.v
index 86f24b1cbe..ff850ea574 100644
--- a/contrib/cc/CC.v
+++ b/contrib/cc/CC.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $id:$ *)
+(* $Id$ *)
-(* Here were some now deprecated lemmata *)
+(* Here were some deprecated lemmata *)
Tactic Definition CCsolve :=
Repeat (Match Context With