Universes introduction

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualParser.mly

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index 3ca69d5c6d59ba9f0fd3701942f6c58a8f8ba97f..41a36acc6ae7e3f624905f50c15c1ceba12936d4 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -136,12 +136,14 @@
 
  let mk_implicit () =
   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
      TexCicTextualParser0.metasenv :=
-      [newmeta, new_canonical_context, Sort Type ;
+      [newmeta, new_canonical_context, Sort (Type newuniv);
+       (* TASSI: ?? *)
        newmeta+1, new_canonical_context, Meta (newmeta,irl);
        newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
       ] @ !TexCicTextualParser0.metasenv ;
@@ -422,7 +424,7 @@ expr2:
     { mk_implicit () }
  | SET   { [], function _ -> Sort Set }
  | PROP  { [], function _ -> Sort Prop }
- | TYPE  { [], function _ -> Sort Type }
+ | TYPE  { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)}
  | CPROP { [], function _ -> Sort CProp }
  | LPAREN expr CAST expr RPAREN
     { let dom1,mk_expr1 = $2 in
@@ -562,12 +564,14 @@ pihead:
     { TexCicTextualParser0.binders :=
        (Some (Name $2))::!TexCicTextualParser0.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
          TexCicTextualParser0.metasenv :=
-          [newmeta, new_canonical_context, Sort Type ;
+          [newmeta, new_canonical_context, Sort (Type newuniv);
+          (* TASSI: ?? *)
            newmeta+1, new_canonical_context, Meta (newmeta,irl)
           ] @ !TexCicTextualParser0.metasenv ;
          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
@@ -584,12 +588,14 @@ lambdahead:
     { TexCicTextualParser0.binders :=
        (Some (Name $2))::!TexCicTextualParser0.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
          TexCicTextualParser0.metasenv :=
-          [newmeta, new_canonical_context, Sort Type ;
+          [newmeta, new_canonical_context, Sort (Type newuniv) ;
+          (* TASSI: ?? *)
            newmeta+1, new_canonical_context, Meta (newmeta,irl)
           ] @ !TexCicTextualParser0.metasenv ;
          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))