X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=a869bc0689f1d4ecf1960504ac7ac58b2ce42bf3;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=08d85a595a2b03c358f07586ffdd4eb86ab5c30a;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 08d85a595..a869bc068 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -135,13 +135,15 @@
  ;;
 
  let mk_implicit () =
+  let newuniv = CicUniv.fresh () in
+  (* TASSI: what is an implicit? *)
   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, new_canonical_context, Sort (Type newuniv);
        newmeta+1, new_canonical_context, Meta (newmeta,irl);
        newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
       ] @ !CicTextualParser0.metasenv ;
@@ -155,7 +157,7 @@
 %token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
@@ -286,9 +288,10 @@ expr2:
     }
  | IMPLICIT
     { mk_implicit () }
- | SET  { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
+ | SET   { [], function _ -> Sort Set }
+ | PROP  { [], function _ -> Sort Prop }
+ | TYPE  { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)}
+ | CPROP { [], function _ -> Sort CProp }
  | LPAREN expr CAST expr RPAREN
     { let dom1,mk_expr1 = $2 in
       let dom2,mk_expr2 = $4 in
@@ -424,12 +427,14 @@ pihead:
  | PROD ID DOT
     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
       let newmeta = new_meta () in
+      let newuniv = CicUniv.fresh () 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, new_canonical_context, Sort (Type newuniv);
+	   (* TASSI: ?? *)
            newmeta+1, new_canonical_context, Meta (newmeta,irl)
           ] @ !CicTextualParser0.metasenv ;
          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
@@ -444,12 +449,14 @@ lambdahead:
  | LAMBDA ID DOT
     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
       let newmeta = new_meta () in
+      let newuniv = CicUniv.fresh () 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, new_canonical_context, Sort (Type newuniv);
+	   (* TASSI: ?? *)
            newmeta+1, new_canonical_context, Meta (newmeta,irl)
           ] @ !CicTextualParser0.metasenv ;
          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))