- Fix hashing of levels to get the "right" order in universe contexts etc...

- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.

1 files changed, 11 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d8cf9fd161..7f13fff2cf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -748,9 +748,9 @@ let intern_reference ref =
   Smartlocate.global_of_extended_global r
 
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid intern env lvar args =
+let intern_qualid loc qid intern env lvar us args =
   match intern_extended_global_of_qualid (loc,qid) with
-  | TrueGlobal ref -> GRef (loc, ref, None), args
+  | TrueGlobal ref -> GRef (loc, ref, us), args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
@@ -763,15 +763,15 @@ let intern_qualid loc qid intern env lvar args =
       subst_aconstr_in_glob_constr loc intern lvar subst infos c, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid intern env lvar args =
-  match intern_qualid loc qid intern env lvar args with
+let intern_non_secvar_qualid loc qid intern env lvar us args =
+  match intern_qualid loc qid intern env lvar us args with
     | GRef (_, VarRef _, _),_ -> raise Not_found
     | r -> r
 
-let intern_applied_reference intern env namedctx lvar args = function
+let intern_applied_reference intern env namedctx lvar us args = function
   | Qualid (loc, qid) ->
       let r,args2 =
-	try intern_qualid loc qid intern env lvar args
+	try intern_qualid loc qid intern env lvar us args
 	with Not_found -> error_global_not_found_loc loc qid
       in
       let x, isproj, imp, scopes, l = find_appl_head_data r in
@@ -781,7 +781,7 @@ let intern_applied_reference intern env namedctx lvar args = function
       with Not_found ->
       let qid = qualid_of_ident id in
       try
-	let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
+	let r,args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
 	let x, isproj, imp, scopes, l = find_appl_head_data r in
 	  (x,imp,scopes,l), isproj, args2
       with Not_found ->
@@ -795,7 +795,7 @@ let interp_reference vars r =
     intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
-      (vars, Id.Map.empty) [] r
+      (vars, Id.Map.empty) None [] r
   in r
 
 (**********************************************************************)
@@ -1368,7 +1368,7 @@ let internalize globalenv env allow_patvar lvar c =
   let rec intern env = function
     | CRef (ref,us) as x ->
 	let (c,imp,subscopes,l),isproj,_ =
-	  intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
+	  intern_applied_reference intern env (Environ.named_context globalenv) lvar us [] ref in
 	  apply_impargs (None, isproj) c env imp subscopes l (constr_loc x)
 
     | CFix (loc, (locid,iddef), dl) ->
@@ -1467,7 +1467,7 @@ let internalize globalenv env allow_patvar lvar c =
         let (f,_,args_scopes,_),_,args =
 	  let args = List.map (fun a -> (a,None)) args in
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
-	    lvar args ref in
+	    lvar us args ref in
 	(* check_projection isproj (List.length args) f; *)
 	(* Rem: GApp(_,f,[]) stands for @f *)
 	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
@@ -1483,7 +1483,7 @@ let internalize globalenv env allow_patvar lvar c =
           match f with
             | CRef (ref,us) -> 
 	       intern_applied_reference intern env
-		 (Environ.named_context globalenv) lvar args ref
+		 (Environ.named_context globalenv) lvar us args ref
             | CNotation (loc,ntn,([],[],[])) ->
                 let c = intern_notation intern env lvar loc ntn ([],[],[]) in
                 let x, isproj, impl, scopes, l = find_appl_head_data c in