Merge branch 'v8.5'

6 files changed, 71 insertions, 42 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 616ceeabdc..f388f90057 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
-      let evd, b = 
-	try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 
-	with Univ.UniverseInconsistency _ -> evd, false
+      let evd, e = 
+	try
+	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
+	    env evd term1 term2 
+	  in
+	    if b then evd, None
+	    else evd, Some (ConversionFailed (env,term1,term2))
+	with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e)
       in
-	if b then Some (evd, true)
-	else if is_ground_env evd env then Some (evd, false)
-	else None)
+	match e with
+	| None -> Some (evd, e)
+	| Some e -> 
+	  if is_ground_env evd env then Some (evd, Some e)
+	  else None)
     else None
   in
   match ground_test with
-    | Some (evd, true) -> Success evd
-    | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+    | Some (evd, None) -> Success evd
+    | Some (evd, Some e) -> UnifFailure (evd,e)
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f355d9a725..bfd19c6c7d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -179,23 +179,30 @@ let restrict_instance evd evk filter argsv =
 
 let noccur_evar env evd evk c =
   let cache = ref Int.Set.empty (* cache for let-ins *) in
-  let rec occur_rec k c =
+  let rec occur_rec (k, env as acc) c =
   match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec k c
+       | Some c -> occur_rec acc c
        | None ->
            if Evar.equal evk evk' then raise Occur
-           else Array.iter (occur_rec k) args')
+           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-k) env) with
+      (match pi2 (Environ.lookup_rel i env) with
        | None -> ()
-       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec k (lift i b))
-  | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
-  | _ -> iter_constr_with_binders succ occur_rec k c
+       | Some 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 []
+      with Retyping.RetypeError _ -> 
+	(* Can happen when called from w_unify which doesn't assign evars/metas 
+	   eagerly enough *) c
+    in occur_rec acc c
+  | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
+    occur_rec acc c
   in
-  try occur_rec 0 c; true with Occur -> false
+  try occur_rec (0,env) c; true with Occur -> false
 
 (***************************************)
 (* Managing chains of local definitons *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c49bec9aec..009b7323e4 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with
 
 let pattern_of_constr env sigma t =
   let ctx = ref [] in
+  let keep = ref Evar.Set.empty in
+  let remove = ref Evar.Set.empty in
   let rec pattern_of_constr env t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -141,28 +143,35 @@ let pattern_of_constr env sigma t =
     | App (f,a) ->
         (match
           match kind_of_term f with
-            Evar (evk,args as ev) ->
-              (match snd (Evd.evar_source evk sigma) with
-                  Evar_kinds.MatchingVar (true,id) ->
-                    ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-                    Some id
-                | _ -> None)
-            | _ -> None
-          with
-            | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
-            | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
+          | Evar (evk,args as ev) ->
+            (match snd (Evd.evar_source evk sigma) with
+              Evar_kinds.MatchingVar (true,id) ->
+		let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+                  ctx := (id,None,ty)::!ctx;
+		  keep := Evar.Set.union (evars_of_term ty) !keep;
+		  remove := Evar.Set.add evk !remove;
+                  Some id
+            | _ -> None)
+          | _ -> None
+         with
+         | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
+         | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
       pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
-        (match snd (Evd.evar_source evk sigma) with
-          | Evar_kinds.MatchingVar (b,id) ->
-              ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-              assert (not b); PMeta (Some id)
-          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt)
-          | _ -> PMeta None)
+      remove := Evar.Set.add evk !remove;
+      (match snd (Evd.evar_source evk sigma) with
+      | Evar_kinds.MatchingVar (b,id) ->
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+          ctx := (id,None,ty)::!ctx;
+	  keep := Evar.Set.union (evars_of_term ty) !keep;
+          assert (not b); PMeta (Some id)
+      | Evar_kinds.GoalEvar -> 
+	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | _ -> PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
@@ -178,9 +187,11 @@ let pattern_of_constr env sigma t =
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
   let p = pattern_of_constr env t in
+  let remove = Evar.Set.diff !remove !keep in
+  let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
   (* side-effect *)
   (* Warning: the order of dependencies in ctx is not ensured *)
-  (!ctx,p)
+  (sigma,!ctx,p)
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -220,7 +231,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  snd (pattern_of_constr env sigma c)
+	  pi3 (pattern_of_constr env sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -245,7 +256,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 snd (pattern_of_constr (Global.env()) Evd.empty t)
+	 pi3 (pattern_of_constr (Global.env()) Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cf02421c24..9e72280fe2 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 
+  Evd.evar_map * named_context * constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 09eb38bd12..dd671f111e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -994,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
 	|_ -> fold ()
       else fold ()
@@ -1073,7 +1073,7 @@ let local_whd_state_gen flags sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
 	|_ -> s
       else s
@@ -1293,7 +1293,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
+let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
+    env sigma x y = 
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1315,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ -> sigma, false
+  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d4f061c5be..1df2a73b2e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 
 (** [infer_fconv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
+    @raises UniverseInconsistency iff catch_incon is set to false, 
+    otherwise returns false in that case.
  *)
-val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> 
-  evar_map * bool
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
+  env -> evar_map -> constr -> constr -> evar_map * bool
 
 (** {6 Special-Purpose Reduction Functions } *)