Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 173 insertions, 102 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ac1692f451..3d1822102a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,7 +11,6 @@ open Errors
 open Names
 open Term
 open Vars
-open Context
 open Environ
 open Termops
 open Evd
@@ -20,6 +19,8 @@ open Retyping
 open Reductionops
 open Evarutil
 open Pretype_errors
+open Sigma.Notations
+open Context.Rel.Declaration
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -42,21 +43,20 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-(**
-   forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed
-   hd ?A (l : list t) -> A = t
+let refresh_level evd s =
+  match Evd.is_sort_variable evd s with
+  | None -> true
+  | Some l -> not (Evd.is_flexible_level evd l)
 
-*)
-let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh dir t = 
+  let rec refresh status dir t = 
     match kind_of_term t with
     | Sort (Type u as s) when
       (match Univ.universe_level u with
-      | None -> true 
-      | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) ->
-    let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in
+      | None -> true
+      | Some l -> not onlyalg && refresh_level evd s) ->
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
       if dir then set_leq_sort env !evdref s' s
@@ -64,11 +64,11 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     in
       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
-      mkProd (na,u,refresh dir v)
+      mkProd (na,u,refresh status dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
-    match kind_of_term t with
+    match kind_of_term (whd_evar !evdref t) with
     | App (f, args) when is_template_polymorphic env f ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
@@ -77,11 +77,11 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh true evi.evar_concl in
+      let ty' = refresh univ_flexible true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
-    | _ -> iter_constr (refresh_term_evars onevars false) t
+    | _ -> Constr.iter (refresh_term_evars onevars false) t
   and refresh_polymorphic_positions args pos =
     let rec aux i = function
       | Some l :: ls -> 
@@ -99,7 +99,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     if isArity t then
       (match pbty with
       | None -> t
-      | Some dir -> refresh dir t)
+      | Some dir -> refresh status dir t)
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
@@ -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,34 @@ 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 *)
+
+exception IllTypedInstance of env * types * types
+
+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))
+	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
+       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         *
  *------------------------------------*)
@@ -135,7 +164,8 @@ type 'a update =
 | UpdateWith of 'a
 | NoUpdate
 
-let inst_of_vars sign = Array.map_of_list (fun (id,_,_) -> mkVar id) sign
+open Context.Named.Declaration
+let inst_of_vars sign = Array.map_of_list (mkVar % get_id) sign
 
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
@@ -153,7 +183,9 @@ let restrict_evar_key evd evk filter candidates =
       let candidates = match candidates with
       | NoUpdate -> evi.evar_candidates
       | UpdateWith c -> Some c in
-      restrict_evar evd evk filter candidates
+      let sigma = Sigma.Unsafe.of_evar_map evd in
+      let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
+      (Sigma.to_evar_map sigma, evk)
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
@@ -178,6 +210,7 @@ let restrict_instance evd evk filter argsv =
   let evi = Evd.find evd evk in
   Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
 
+open Context.Rel.Declaration
 let noccur_evar env evd evk c =
   let cache = ref Int.Set.empty (* cache for let-ins *) in
   let rec occur_rec (k, env as acc) c =
@@ -190,9 +223,9 @@ let noccur_evar env evd evk c =
            else Array.iter (occur_rec acc) args')
   | Rel i when i > k ->
       if not (Int.Set.mem (i-k) !cache) then
-      (match pi2 (Environ.lookup_rel i env) with
-       | None -> ()
-       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
+      (match Environ.lookup_rel i env with
+       | LocalAssum _ -> ()
+       | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
   | Proj (p,c) -> 
     let c = 
       try Retyping.expand_projection env evd p c []
@@ -214,9 +247,11 @@ let noccur_evar env evd evk c =
    variable in its family of aliased variables *)
 
 let compute_var_aliases sign =
-  List.fold_right (fun (id,b,c) aliases ->
-    match b with
-    | Some t ->
+  let open Context.Named.Declaration in
+  List.fold_right (fun decl aliases ->
+    let id = get_id decl in
+    match decl with
+    | LocalDef (_,t,_) ->
         (match kind_of_term t with
         | Var id' ->
             let aliases_of_id =
@@ -224,27 +259,30 @@ let compute_var_aliases sign =
             Id.Map.add id (aliases_of_id@[t]) aliases
         | _ ->
             Id.Map.add id [t] aliases)
-    | None -> aliases)
+    | LocalAssum _ -> aliases)
     sign Id.Map.empty
 
 let compute_rel_aliases var_aliases rels =
-  snd (List.fold_right (fun (_,b,u) (n,aliases) ->
-    (n-1,
-     match b with
-     | Some t ->
-         (match kind_of_term t with
-         | Var id' ->
-             let aliases_of_n =
-               try Id.Map.find id' var_aliases with Not_found -> [] in
-             Int.Map.add n (aliases_of_n@[t]) aliases
-         | Rel p ->
-             let aliases_of_n =
-               try Int.Map.find (p+n) aliases with Not_found -> [] in
-             Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
-         | _ ->
-             Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
-     | None -> aliases))
-         rels (List.length rels,Int.Map.empty))
+  snd (List.fold_right
+	 (fun decl (n,aliases) ->
+	  (n-1,
+	   match decl with
+	   | LocalDef (_,t,u) ->
+	      (match kind_of_term t with
+	       | Var id' ->
+		  let aliases_of_n =
+		    try Id.Map.find id' var_aliases with Not_found -> [] in
+		  Int.Map.add n (aliases_of_n@[t]) aliases
+	       | Rel p ->
+		  let aliases_of_n =
+		    try Int.Map.find (p+n) aliases with Not_found -> [] in
+		  Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
+	       | _ ->
+		  Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
+	   | LocalAssum _ -> aliases)
+	 )
+	 rels
+	 (List.length rels,Int.Map.empty))
 
 let make_alias_map env =
   (* We compute the chain of aliases for each var and rel *)
@@ -278,13 +316,13 @@ let normalize_alias aliases x =
 let normalize_alias_var var_aliases id =
   destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id))
 
-let extend_alias (_,b,_) (var_aliases,rel_aliases) =
+let extend_alias decl (var_aliases,rel_aliases) =
   let rel_aliases =
     Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
       rel_aliases Int.Map.empty in
   let rel_aliases =
-    match b with
-    | Some t ->
+    match decl with
+    | LocalDef(_,t,_) ->
         (match kind_of_term t with
         | Var id' ->
             let aliases_of_binder =
@@ -296,7 +334,7 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
             Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
         | _ ->
             Int.Map.add 1 [lift 1 t] rel_aliases)
-    | None -> rel_aliases in
+    | LocalAssum _ -> rel_aliases in
   (var_aliases, rel_aliases)
 
 let expand_alias_once aliases x =
@@ -402,16 +440,17 @@ let get_actual_deps aliases l t =
       | Rel n -> Int.Set.mem n fv_rels
       | _ -> assert false) l
 
+open Context.Named.Declaration
 let remove_instance_local_defs evd evk args =
   let evi = Evd.find evd evk in
   let len = Array.length args in
   let rec aux sign i = match sign with
   | [] ->
     let () = assert (i = len) in []
-  | (_, None, _) :: sign ->
+  | LocalAssum _ :: sign ->
     let () = assert (i < len) in
     (Array.unsafe_get args i) :: aux sign (succ i)
-  | (_, Some _, _) :: sign ->
+  | LocalDef _ :: sign ->
     aux sign (succ i)
   in
   aux (evar_filtered_context evi) 0
@@ -473,7 +512,8 @@ let solve_pattern_eqn env l c =
     match kind_of_term a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
-          let d = map_rel_declaration (lift n) (lookup_rel n env) in
+          let open Context.Rel.Declaration in
+          let d = map_constr (lift n) (lookup_rel n env) in
           mkLambda_or_LetIn d c'
       | Var id ->
           let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
@@ -502,9 +542,9 @@ let make_projectable_subst aliases sigma evi args =
   let evar_aliases = compute_var_aliases sign in
   let (_,full_subst,cstr_subst) =
     List.fold_right
-      (fun (id,b,c) (args,all,cstrs) ->
-        match b,args with
-        | None, a::rest ->
+      (fun decl (args,all,cstrs) ->
+        match decl,args with
+        | LocalAssum (id,c), a::rest ->
             let a = whd_evar sigma a in
             let cstrs =
               let a',args = decompose_app_vect a in
@@ -514,7 +554,7 @@ let make_projectable_subst aliases sigma evi args =
                   Constrmap.add (fst cstr) ((args,id)::l) cstrs
               | _ -> cstrs in
             (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
-        | Some c, a::rest ->
+        | LocalDef (id,c,_), a::rest ->
             let a = whd_evar sigma a in
             (match kind_of_term c with
             | Var id' ->
@@ -543,7 +583,9 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
-  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let evd = Sigma.to_evar_map evd in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -574,23 +616,26 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
   let src = subterm_source evk1 evi1.evar_source in
-  let ids1 = List.map pi1 (named_context_of_val sign1) in
+  let ids1 = List.map get_id (named_context_of_val sign1) in
   let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
+  let open Context.Rel.Declaration in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
-    List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
+    List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
+      let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in
       let id = next_name_away na avoid in
       let evd,t_in_sign =
         let s = Retyping.get_sort_of env evd t_in_env in
-        let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
+        let evd,ty_t_in_sign = refresh_universes
+	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
-      let evd,b_in_sign = match b with
-      | None -> evd,None
-      | Some b ->
+      let evd,b_in_sign = match d with
+      | LocalAssum _ -> evd,None
+      | LocalDef (_,b,_) ->
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
           evd,Some b in
-      (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.extend 1 filter,
+      (push_named_context_val (Context.Named.Declaration.of_tuple (id,b_in_sign,t_in_sign)) sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
        push_rel d env,evd,id::avoid))
@@ -599,11 +644,14 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
-    let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
+    let evd,ty_t_in_sign = refresh_universes
+     ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
-  let evd,ev2_in_sign =
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (ev2_in_sign, evd, _) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
+  let evd = Sigma.to_evar_map evd in
   let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
@@ -727,9 +775,10 @@ let project_with_effects aliases sigma effects t subst =
   effects := p :: !effects;
   c
 
+open Context.Named.Declaration
 let rec find_solution_type evarenv = function
-  | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
-  | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
+  | (id,ProjectVar)::l -> get_type (lookup_named id evarenv)
+  | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv)
   | (id,ProjectEvar _)::l -> find_solution_type evarenv l
   | [] -> assert false
 
@@ -863,7 +912,7 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
  *)
 
 let set_of_evctx l =
-  List.fold_left (fun s (id,_,_) -> Id.Set.add id s) Id.Set.empty l
+  List.fold_left (fun s decl -> Id.Set.add (get_id decl) s) Id.Set.empty l
 
 let filter_effective_candidates evi filter candidates =
   match filter with
@@ -895,7 +944,13 @@ let closure_of_filter evd evk = function
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
-  let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in
+  let test b decl = b || Idset.mem (get_id decl) vars ||
+                    match decl with
+                    | LocalAssum _ ->
+                       false
+                    | LocalDef (_,c,_) ->
+                       not (isRel c || isVar c)
+  in
   let newfilter = Filter.map_along test filter (evar_context evi) in
   (* Now ensure that restriction is at least what is was originally *)
   let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in
@@ -977,21 +1032,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
  * Note: argument f is the function used to instantiate evars.
  *)
 
-let are_canonical_instances args1 args2 env =
-  let n1 = Array.length args1 in
-  let n2 = Array.length args2 in
-  let rec aux n = function
-    | (id,_,c)::sign
-        when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
-        aux (n+1) sign
-    | [] ->
-        let rec aux2 n =
-          Int.equal n n1 ||
-          (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
-        in aux2 n
-    | _ -> false in
-  Int.equal n1 n2 && aux 0 (named_context env)
-
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
   match conv_algo env evd Reduction.CONV rhs c' with
@@ -1107,8 +1147,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   else
     raise (CannotProject (evd,ev1'))
 
-exception IllTypedInstance of env * types * types
-
 let check_evar_instance evd evk1 body conv_algo =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
@@ -1122,10 +1160,19 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
+let update_evar_source ev1 ev2 evd =
+  let loc, evs2 = evar_source ev2 evd in
+  match evs2 with
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) ->
+     let evi = Evd.find evd ev1 in
+     Evd.add evd ev1 {evi with evar_source = loc, evs2}
+  | _ -> evd
+  
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 body evd in
+    let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
@@ -1137,8 +1184,8 @@ let preferred_orientation evd evk1 evk2 =
   let _,src2 = (Evd.find_undefined evd evk2).evar_source in
   (* This is a heuristic useful for program to work *)
   match src1,src2 with
-  | Evar_kinds.QuestionMark _, _ -> true
-  | _,Evar_kinds.QuestionMark _ -> false
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
+  | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
   | _ -> true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
@@ -1239,12 +1286,30 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
       | [c,evd] ->
           (* solve_candidates might have been called recursively in the mean *)
           (* time and the evar been solved by the filtering process *)
-          if Evd.is_undefined evd evk then Evd.define evk c evd else evd
+         if Evd.is_undefined evd evk then
+	   let evd' = Evd.define evk c evd in
+	     check_evar_instance evd' evk c conv_algo
+	 else evd
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
           restrict_evar evd evk None (UpdateWith candidates)
       | l -> evd
 
+let occur_evar_upto_types sigma n c =
+  let seen = ref Evar.Set.empty in
+  let rec occur_rec c = match kind_of_term c with
+    | Evar (sp,_) when Evar.equal sp n -> raise Occur
+    | Evar (sp,args as e) ->
+       if Evar.Set.mem sp !seen then
+         Array.iter occur_rec args
+       else (
+         seen := Evar.Set.add sp !seen;
+	 Option.iter occur_rec (existential_opt_value sigma e);
+	 occur_rec (existential_type sigma e))
+    | _ -> Constr.iter occur_rec c
+  in
+  try occur_rec c; false with Occur -> true
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
@@ -1326,15 +1391,16 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
     let t = whd_evar !evdref t in
     match kind_of_term t with
     | Rel i when i>k ->
-        (match pi2 (Environ.lookup_rel (i-k) env') with
-        | None -> project_variable (mkRel (i-k))
-        | Some b ->
+        let open Context.Rel.Declaration in
+        (match Environ.lookup_rel (i-k) env' with
+        | LocalAssum _ -> project_variable (mkRel (i-k))
+        | LocalDef (_,b,_) ->
           try project_variable (mkRel (i-k))
           with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
     | Var id ->
-        (match pi2 (Environ.lookup_named id env') with
-        | None -> project_variable t
-        | Some b ->
+        (match Environ.lookup_named id env' with
+        | LocalAssum _ -> project_variable t
+        | LocalDef (_,b,_) ->
           try project_variable t
           with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
     | LetIn (na,b,u,c) ->
@@ -1404,17 +1470,18 @@ 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
     let names = ref Idset.empty in
     let rec is_id_subst ctxt s =
       match ctxt, s with
-      | ((id, _, _) :: ctxt'), (c :: s') ->
+      | (decl :: ctxt'), (c :: s') ->
+        let id = get_id decl in
         names := Idset.add id !names;
         isVarId id c && is_id_subst ctxt' s'
       | [], [] -> true
@@ -1426,9 +1493,13 @@ 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,
  * [define] tries to find an instance lhs such that
@@ -1453,7 +1524,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm