Merge branch 'v8.5'

3 files changed, 60 insertions, 16 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ac1692f45..a2189d5e4 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -107,6 +107,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
     refresh_universes (Some false) env sigma ty
+		      
 
 (************************)
 (* Unification results  *)
@@ -127,6 +128,32 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
   | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
 
+(* We retype applications to ensure the universe constraints are collected *)
+
+let recheck_applications conv_algo env evdref t =
+  let rec aux env t =
+    match kind_of_term t with
+    | App (f, args) ->
+       let () = aux env f in
+       let fty = Retyping.get_type_of env !evdref f in
+       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
+       let rec aux i ty =
+	 if i < Array.length argsty then
+	 match kind_of_term (whd_betadeltaiota env !evdref ty) with
+	 | Prod (na, dom, codom) ->
+	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
+	     | Success evd -> evdref := evd;
+			     aux (succ i) (subst1 args.(i) codom)
+	     | UnifFailure (evd, reason) ->
+		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
+	 | _ -> assert false
+       else ()
+     in aux 0 fty
+    | _ ->
+       iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t
+  in aux env t
+
+	  
 (*------------------------------------*
  * Restricting existing evars         *
  *------------------------------------*)
@@ -1404,10 +1431,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
               evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates);
               evar'')
         | None ->
-          (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-            map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-              imitate envk t in
-
+           (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
+	   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+					imitate envk t
+  in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
@@ -1426,8 +1453,12 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
   in
   let body =
     if fast rhs then nf_evar evd rhs
-    else imitate (env,0) rhs
- in (!evdref,body)
+    else
+      let t' = imitate (env,0) rhs in
+	if !progress then
+	  (recheck_applications conv_algo (evar_env evi) evdref t'; t')
+	else t'
+  in (!evdref,body)
 
 (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2858a5c1f..f18657da8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -102,14 +102,27 @@ let ((constr_in : constr -> Dyn.t),
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd s =
   let names, _ = Universes.global_universe_names () in
-  try
-    let id = try Id.of_string s with _ -> raise Not_found in
-      evd, Idmap.find id names
-  with Not_found ->
-    try let level = Evd.universe_of_name evd s in
-	  evd, level
-    with Not_found -> 
-      new_univ_level_variable ~name:s univ_rigid evd
+    if CString.string_contains s "." then
+      match List.rev (CString.split '.' s) with
+      | [] -> anomaly (str"Invalid universe name " ++ str s)
+      | n :: dp -> 
+	 let num = int_of_string n in
+	 let dp = DirPath.make (List.map Id.of_string dp) in
+	 let level = Univ.Level.make dp num in
+	 let evd =
+	   try Evd.add_global_univ evd level
+	   with Univ.AlreadyDeclared -> evd
+	 in evd, level
+    else 
+      try
+	let id =
+	  try Id.of_string s with _ -> raise Not_found in
+	  evd, Idmap.find id names
+      with Not_found ->
+	try let level = Evd.universe_of_name evd s in
+	      evd, level
+	with Not_found -> 
+	  new_univ_level_variable ~name:s univ_rigid evd
 
 let interp_universe evd = function
   | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
@@ -632,7 +645,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
         let f = whd_evar !evdref f in
-          if isInd f && is_template_polymorphic env f then
+          if is_template_polymorphic env f then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
 	    let sigma = !evdref in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 18e83056b..2ef289650 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -370,7 +370,7 @@ let add_instance check inst =
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
     (is_local inst) pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
-       (Global.env ()) Evd.empty inst.is_impl inst.is_pri)
+       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
 
 let rebuild_instance (action, inst) =
   let () = match action with