diff options
Diffstat (limited to 'syntax/PPTactic.v')
| -rw-r--r-- | syntax/PPTactic.v | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index e97df073f6..62c3319a0c 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -1,17 +1,5 @@ -(****************************************************************************) -(* The Calculus of Inductive Constructions *) -(* *) -(* Projet Coq *) -(* *) -(* INRIA LRI-CNRS ENS-CNRS *) -(* Rocquencourt Orsay Lyon *) -(* *) -(* Coq V6.3 *) -(* July 1st 1999 *) -(* *) -(****************************************************************************) -(* PPTactic.v *) -(****************************************************************************) + +(* $Id$ *) (* ======================================= *) (* PP rules for basic elements *) @@ -325,6 +313,3 @@ Syntax tactic level 8: command [(COMMAND $c)] -> [ (PPUNI$COMMAND $c):E ]. - - -(* $Id$ *) |