From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 22 Dec 2002 19:05:38 +0000 (+0000)
Subject: New constructs \x.T and !x.T introduced. They require refinement.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bdf8492f9e68500178dccde1c6f8614296f7c7dc;p=helm.git

New constructs \x.T and !x.T introduced. They require refinement.
---

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index bb9113403..1d4bd933d 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -410,13 +410,39 @@ pihead:
      let dom,mk_expr = $2 in
       Anonymous, (dom, function interp -> mk_expr interp)
    }
+ | PROD ID DOT
+    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
+      let newmeta = new_meta () in
+       let new_canonical_context = [] in
+        let irl =
+         identity_relocation_list_for_metavariable new_canonical_context
+        in
+         CicTextualParser0.metasenv :=
+          [newmeta, new_canonical_context, Sort Type ;
+           newmeta+1, new_canonical_context, Meta (newmeta,irl)
+          ] @ !CicTextualParser0.metasenv ;
+         Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
+    }
 ;
 lambdahead:
-  LAMBDA ID COLON expr DOT
-   { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
-     let dom,mk_expr = $4 in
-      Cic.Name $2, (dom, function interp -> mk_expr interp)
-   }
+   LAMBDA ID COLON expr DOT
+    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
+      let dom,mk_expr = $4 in
+       Cic.Name $2, (dom, function interp -> mk_expr interp)
+    }
+ | LAMBDA ID DOT
+    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
+      let newmeta = new_meta () in
+       let new_canonical_context = [] in
+        let irl =
+         identity_relocation_list_for_metavariable new_canonical_context
+        in
+         CicTextualParser0.metasenv :=
+          [newmeta, new_canonical_context, Sort Type ;
+           newmeta+1, new_canonical_context, Meta (newmeta,irl)
+          ] @ !CicTextualParser0.metasenv ;
+         Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
+    }
 ;
 letinhead:
   LAMBDA ID LETIN expr DOT