Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

16 files changed, 95 insertions, 54 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bdf94e0d..86f96c7c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -126,7 +126,7 @@ module Default = struct
 		     jres),
 		jres.uj_type)
              (hj,typ_cl) p)
-    with _ -> anomaly "apply_coercion"
+    with e when Errors.noncritical e -> anomaly "apply_coercion"
 
   let inh_app_fun env evd j =
     let t = whd_betadeltaiota env evd j.uj_type in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a74e4cb4..0166b64c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -272,7 +272,7 @@ let is_nondep_branch c n =
   try
     let sign,ccl = decompose_lam_n_assum n c in
     noccur_between 1 (rel_context_length sign) ccl
-  with _ -> (* Not eta-expanded or not reduced *)
+  with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
 let extract_nondep_branches test c b n =
@@ -386,7 +386,7 @@ let rec detype (isgoal:bool) avoid env t =
     | Var id ->
 	(try
 	  let _ = Global.lookup_named id in GRef (dl, VarRef id)
-	 with _ ->
+	 with e when Errors.noncritical e ->
 	  GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
@@ -492,7 +492,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
     let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
     List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
       mat
-  with _ ->
+  with e when Errors.noncritical e ->
     Array.to_list
       (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 14f35941..0eed1949 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -454,7 +454,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 		 else Evd.set_leq_sort evd s1 s2 
 	       in (evd', true)
 	     with Univ.UniverseInconsistency _ -> (evd, false)
-	     | _ -> (evd, false))
+	     | e when Errors.noncritical e -> (evd, false))
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
             ise_and evd
@@ -730,12 +730,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = []
-      & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
+      & List.for_all (fun a -> eq_constr a term2 or isEvar a)
+        (remove_instance_local_defs evd evk1 (Array.to_list args1)) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
     choose_less_dependent_instance evk1 evd term2 args1
   | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
-      & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
+      & List.for_all (fun a -> eq_constr a term1 or isEvar a)
+        (remove_instance_local_defs evd evk2 (Array.to_list args2)) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
     choose_less_dependent_instance evk2 evd term1 args2
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b0248a84..fc29ba6c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1194,10 +1194,9 @@ let filter_candidates evd evk filter candidates =
 
 let closure_of_filter evd evk filter =
   let evi = Evd.find_undefined evd evk in
-  let vars = collect_vars (evar_concl evi) in
-  let ids = List.map pi1 (evar_context evi) in
-  let test id b = b || Idset.mem id vars in
-  let newfilter = List.map2 test ids filter in
+  let vars = collect_vars (nf_evar evd (evar_concl evi)) in
+  let test (id,c,_) b = b || Idset.mem id vars || c <> None in
+  let newfilter = List.map2 test (evar_context evi) filter in
   if newfilter = evar_filter evi then None else Some newfilter
 
 let restrict_hyps evd evk filter candidates =
@@ -1352,9 +1351,14 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct (ind,_) ->
-      let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
-      let params,_ = array_chop nparams args in
-      array_for_all (is_constrainable_in k g) params
+      let nparams =
+        (fst (Global.lookup_inductive ind)).Declarations.mind_nparams
+      in
+      if nparams > Array.length args
+      then true (* We don't try to be more clever *)
+      else
+        let params,_ = array_chop nparams args in
+        array_for_all (is_constrainable_in k g) params
   | Ind _ -> array_for_all (is_constrainable_in k g) args
   | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
   | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*)
@@ -1442,7 +1446,7 @@ let check_evar_instance evd evk1 body conv_algo =
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
   let ty =
     try Retyping.get_type_of evenv evd body
-    with _ -> error "Ill-typed evar instance"
+    with e when Errors.noncritical e -> error "Ill-typed evar instance"
   in
   let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
   if b then evd else
@@ -1492,7 +1496,10 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
           (filter_compatible_candidates conv_algo env evd evi args rhs) l in
       match l' with
       | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
-      | [c,evd] -> Evd.define evk c evd
+      | [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
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
           restrict_evar evd evk None (Some candidates)
@@ -1643,7 +1650,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
                   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
 	            imitate envk t in
                 t::l
-              with _ -> l in
+              with e when Errors.noncritical e -> l in
             (match candidates with
             | [x] -> x
             | _ ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 2b326fd1..591a008c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -230,3 +230,4 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun ->
   evar_map
 
+val remove_instance_local_defs : evar_map -> existential_key -> constr list -> constr list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6d5c98ce..4d9eb897 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -67,9 +67,12 @@ let evar_hyps evi = evi.evar_hyps
 let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_body evi = evi.evar_body
 let evar_filter evi = evi.evar_filter
-let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
 let evar_filtered_context evi =
   snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
+let evar_filtered_hyps evi =
+  List.fold_right push_named_context_val (evar_filtered_context evi)
+    empty_named_context_val
+let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
 let evar_env evi =
   List.fold_right push_named (evar_filtered_context evi)
     (reset_context (Global.env()))
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 4813d3b9..dbaf803b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -127,6 +127,7 @@ val evar_concl : evar_info -> constr
 val evar_context : evar_info -> named_context
 val evar_filtered_context : evar_info -> named_context
 val evar_hyps : evar_info -> named_context_val
+val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
 val evar_filter : evar_info -> bool list
 val evar_unfiltered_env :  evar_info -> env
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bb0a0e92..bdccc57b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -290,6 +290,7 @@ let find_rectype env sigma c =
   match kind_of_term t with
     | Ind ind ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
+        if mib.mind_nparams > List.length l then raise Not_found;
         let (par,rargs) = list_chop mib.mind_nparams l in
         IndType((ind, par),rargs)
     | _ -> raise Not_found
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d8678371..1dd71fab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -69,8 +69,9 @@ let search_guard loc env possible_indexes fixdefs =
   if List.for_all (fun l->1=List.length l) possible_indexes then
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
-    (try check_fix env fix with
-       | e -> if loc = dummy_loc then raise e else Loc.raise loc e);
+    (try check_fix env fix
+     with e when Errors.noncritical e ->
+       if loc = dummy_loc then raise e else Loc.raise loc e);
     indexes
   else
     (* we now search recursively amoungst all combinations *)
@@ -109,7 +110,8 @@ let resolve_evars env evdref fail_evar resolve_classes =
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
 	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
-	     with e -> if fail_evar then raise e else !evdref)
+	     with e when Errors.noncritical e ->
+               if fail_evar then raise e else !evdref)
 
 let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
   let evdref = ref evd in
@@ -441,7 +443,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Loc.raise loc e);
+	      (try check_cofix env cofix
+               with e when Errors.noncritical e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 0f04549f..434fe80c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -207,16 +207,16 @@ let cs_pattern_of_constr t =
   match kind_of_term t with
       App (f,vargs) ->
 	begin
-	  try  Const_cs (global_of_constr f) , -1, Array.to_list vargs with
-	      _ -> raise Not_found
+	  try  Const_cs (global_of_constr f) , -1, Array.to_list vargs
+          with e when Errors.noncritical e -> raise Not_found
 	end
     | Rel n -> Default_cs, pred n, []
     | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
     | Sort s -> Sort_cs (family_of_sort s), -1, []
     | _ ->
 	begin
-	  try  Const_cs (global_of_constr t) , -1, [] with
-	      _ -> raise Not_found
+	  try  Const_cs (global_of_constr t) , -1, []
+          with e when Errors.noncritical e -> raise Not_found
 	end
 
 (* Intended to always succeed *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fddc7fc7..993ad46b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -924,7 +924,10 @@ let meta_reducible_instance evd b =
     let u = whd_betaiota Evd.empty u in
     match kind_of_term u with
     | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
-	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+	let m =
+          try destMeta c
+          with e when Errors.noncritical e -> destMeta (pi1 (destCast c))
+        in
 	(match
 	  try
 	    let g,s = List.assoc m metas in
@@ -934,7 +937,10 @@ let meta_reducible_instance evd b =
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
     | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
-	let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
+        let m =
+          try destMeta f
+          with e when Errors.noncritical e -> destMeta (pi1 (destCast f))
+        in
 	(match
 	  try
 	    let g,s = List.assoc m metas in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index f16eed6c..3b679fce 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -30,12 +30,12 @@ let rec subst_type env sigma typ = function
 (* et sinon on substitue *)
 
 let sort_of_atomic_type env sigma ft args =
-  let rec concl_of_arity env ar =
-    match kind_of_term (whd_betadeltaiota env sigma ar) with
-    | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
-    | Sort s -> s
-    | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
-  in concl_of_arity env ft
+  let rec concl_of_arity env ar args =
+    match kind_of_term (whd_betadeltaiota env sigma ar), args with
+    | Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some h,t) env) b l
+    | Sort s, [] -> s
+    | _ -> anomaly "Not a sort"
+  in concl_of_arity env ft (Array.to_list args)
 
 let type_of_var env id =
   try let (_,_,ty) = lookup_named id env in ty
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b43b9adb..78b239c0 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -125,12 +125,12 @@ type constant_evaluation =
 
 (* We use a cache registered as a global table *)
 
-let eval_table = ref Cmap.empty
+let eval_table = ref Cmap_env.empty
 
-type frozen = (int * constant_evaluation) Cmap.t
+type frozen = (int * constant_evaluation) Cmap_env.t
 
 let init () =
-  eval_table := Cmap.empty
+  eval_table := Cmap_env.empty
 
 let freeze () =
   !eval_table
@@ -291,10 +291,10 @@ let compute_consteval sigma env ref =
 let reference_eval sigma env = function
   | EvalConst cst as ref ->
       (try
-	 Cmap.find cst !eval_table
+	 Cmap_env.find cst !eval_table
        with Not_found -> begin
 	 let v = compute_consteval sigma env ref in
-	 eval_table := Cmap.add cst v !eval_table;
+	 eval_table := Cmap_env.add cst v !eval_table;
 	 v
        end)
   | ref -> compute_consteval sigma env ref
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b78850d3..0344ebcc 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -118,7 +118,7 @@ let _ =
 
 let class_info c =
   try Gmap.find c !classes
-  with _ -> not_a_class (Global.env()) (constr_of_global c)
+  with Not_found -> not_a_class (Global.env()) (constr_of_global c)
 
 let global_class_of_constr env c =
   try class_info (global_of_constr c)
@@ -132,7 +132,9 @@ let dest_class_arity env c =
   let rels, c = Term.decompose_prod_assum c in
     rels, dest_class_app env c
 
-let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None
+let class_of_constr c =
+  try Some (dest_class_arity (Global.env ()) c)
+  with e when Errors.noncritical e -> None
 
 let rec is_class_type evd c =
   match kind_of_term c with
@@ -215,7 +217,7 @@ let rebuild_class cl =
   try 
     let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
       set_typeclass_transparency cst false false; cl
-  with _ -> cl
+  with e when Errors.noncritical e -> cl
 
 let class_input : typeclass -> obj =
   declare_object
@@ -238,7 +240,7 @@ let check_instance env sigma c =
     let (evd, c) = resolve_one_typeclass env sigma
       (Retyping.get_type_of env sigma c) in
       Evd.is_empty (Evd.undefined_evars evd)
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let build_subclasses ~check env sigma glob pri =
   let rec aux pri c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 63cdb378..df5eff6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -430,8 +430,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		 then Evd.set_leq_sort sigma s1 s2 
 		 else Evd.set_eq_sort sigma s1 s2 
 	       in (sigma', metasubst, evarsubst)
-	     with _ -> error_cannot_unify curenv sigma (m,n))
-	      
+	     with e when Errors.noncritical e ->
+               error_cannot_unify curenv sigma (m,n))
+
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
 	    unirec_rec (push (na,t1) curenvnb) CONV true wt
 	      (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
@@ -708,10 +709,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
       else (right, st2, res)
   | (IsSuperType,IsSubType) ->
     (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
-     with _ -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
+     with e when Errors.noncritical e ->
+       (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
   | (IsSubType,IsSuperType) ->
     (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
-     with _ -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
+     with e when Errors.noncritical e ->
+       (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
     
 (* Unification
  *
@@ -913,7 +916,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	let rec process_eqns failures = function
 	  | (mv,status,c)::eqns ->
               (match (try Inl (unify_type env evd flags mv status c)
-		      with e -> Inr e)
+		      with e when Errors.noncritical e -> Inr e)
 	       with 
 	       | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
 	       | Inl (evd,metas,evars) ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 00efa981..3966146d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -44,7 +44,7 @@ let invert_tag cst tag reloc_tbl =
 let find_rectype_a env c =
   let (t, l) =
     let t = whd_betadeltaiota env c in
-    try destApp t with _ -> (t,[||]) in
+    try destApp t with e when Errors.noncritical e -> (t,[||]) in
   match kind_of_term t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
@@ -176,7 +176,10 @@ and nf_stk env c t stk  =
       nf_stk env (mkApp(c,args)) t stk
   | Zfix (f,vargs) :: stk ->
       let fa, typ = nf_fix_app env f vargs in
-      let _,_,codom = try decompose_prod env typ with _ -> exit 120 in
+      let _,_,codom =
+        try decompose_prod env typ
+        with e when Errors.noncritical e -> exit 120
+      in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
       let (mind,_ as ind),allargs = find_rectype_a env t in
@@ -206,7 +209,10 @@ and nf_predicate env ind mip params v pT =
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
+      let name,dom,codom =
+        try decompose_prod env pT
+        with e when Errors.noncritical e -> exit 121
+      in
       let dep,body =
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
@@ -228,7 +234,10 @@ and nf_args env vargs t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
+	let _,dom,codom =
+          try decompose_prod env !t
+          with e when Errors.noncritical e -> exit 123
+        in
 	let c = nf_val env (arg vargs i) dom in
 	t := subst1 c codom; c) in
   !t,args
@@ -239,7 +248,10 @@ and nf_bargs env b t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
+	let _,dom,codom =
+          try decompose_prod env !t
+          with e when Errors.noncritical e -> exit 124
+        in
 	let c = nf_val env (bfield b i) dom in
 	t := subst1 c codom; c) in
   args
@@ -249,7 +261,7 @@ and nf_fun env f typ =
   let vb = body_of_vfun k f in
   let name,dom,codom =
     try decompose_prod env typ
-    with _ ->
+    with e when Errors.noncritical e ->
       raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
   in
   let body = nf_val (push_rel (name,None,dom) env) vb codom in