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 bb9113403bd399c80c6d048c29b928eb23db9f35..1d4bd933d151f9a7b8ad7ba8a79dc45eca3a8275 100644 (file)
--- 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