From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Feb 2005 13:45:05 +0000 (+0000)
Subject: Added Coer/Coercions print_kind
X-Git-Tag: V_0_1_0~75
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=caede9392c6fb7988731e0bbd1d1c42817f443de;p=helm.git

Added Coer/Coercions print_kind
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d062ed109..e35101862 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -459,6 +459,8 @@ EXTEND
   print_kind: [
     [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
       -> `Env
+    | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
+      -> `Coer
   ] ];
 
   command: [