;;
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 ;
{ 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
| 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))
| 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))