Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

6 files changed, 88 insertions, 38 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index a145508a..92378837 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -56,12 +56,14 @@ let section_segment_of_reference = function
   | _ -> []
 
 let discharge_rename_args = function
-  | _, (ReqGlobal (c, names), _) ->
-     let c' = pop_global_reference c in
-     let vars = section_segment_of_reference c in
-     let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
-     let names' = List.map (fun l -> var_names @ l) names in
-     Some (ReqGlobal (c', names), (c', names'))
+  | _, (ReqGlobal (c, names), _ as req) ->
+     (try 
+       let vars = section_segment_of_reference c in
+       let c' = pop_global_reference c in
+       let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+       let names' = List.map (fun l -> var_names @ l) names in
+       Some (ReqGlobal (c', names), (c', names'))
+     with Not_found -> Some req)
   | _ -> None
 
 let rebuild_rename_args x = x
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0166b64c..1065aec9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -300,7 +300,7 @@ let it_destRLambda_or_LetIn_names n c =
 	  let a = GVar (dl,x) in
 	  aux (n-1) (Name x :: nal)
             (match c with
-              | GApp (loc,p,l) -> GApp (loc,c,l@[a])
+              | GApp (loc,p,l) -> GApp (loc,p,l@[a])
               | _ -> (GApp (dl,c,[a])))
   in aux n [] c
 
@@ -481,7 +481,7 @@ and share_names isgoal n l avoid env c t =
         share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
-        if n>0 then warning "Detyping.detype: cannot factorize fix enough";
+        if n>0 then msg_warn "Detyping.detype: cannot factorize fix enough";
         let c = detype isgoal avoid env c in
         let t = detype isgoal avoid env t in
         (List.rev l,c,t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0eed1949..f0019448 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -197,6 +197,18 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false)
   ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
+
+  let eta env evd onleft term l term' l' =
+    assert (l = []);
+    let (na,c,body) = destLambda term in
+    let c = nf_evar evd c in
+    let env' = push_rel (na,None,c) env in
+    let appr1 = evar_apprec ts env' evd [] body in
+    let appr2 = (lift 1 term', List.map (lift 1) l' @ [mkRel 1]) in
+    if onleft then evar_eqappr_x ts env' evd CONV appr1 appr2
+    else evar_eqappr_x ts env' evd CONV appr2 appr1
+  in
+
   (* Evar must be undefined since we have flushed evars *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -382,6 +394,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,ev1,t2)
         | None ->
+          if isLambda term2 then
+            eta env evd false term2 l2 term1 l1
+          else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true)
@@ -396,6 +411,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,ev2,t1)
         | None ->
+          if isLambda term1 then
+            eta env evd true term1 l1 term2 l2
+          else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true)
@@ -408,7 +426,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
-	    | None -> (i,false)
+	    | None ->
+                if isLambda term2 then
+                  eta env i false term2 l2 term1 l1
+                else
+                  (i,false)
 	in
 	ise_try evd [f3; f4]
 
@@ -420,28 +442,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
-	    | None -> (i,false)
+	    | None ->
+                if isLambda term1 then
+                  eta env i true term1 l1 term2 l2
+                else
+                  (i,false)
 	in
 	ise_try evd [f3; f4]
 
     (* Eta-expansion *)
     | Rigid c1, _ when isLambda c1 ->
-	assert (l1 = []);
-	let (na,c1,c'1) = destLambda c1 in
-        let c = nf_evar evd c1 in
-	let env' = push_rel (na,None,c) env in
-        let appr1 = evar_apprec ts env' evd [] c'1 in
-	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
-	evar_eqappr_x ts env' evd CONV appr1 appr2
+        eta env evd true term1 l1 term2 l2
 
     | _, Rigid c2 when isLambda c2 ->
-	assert (l2 = []);
-	let (na,c2,c'2) = destLambda c2 in
-        let c = nf_evar evd c2 in
-	let env' = push_rel (na,None,c) env in
-	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
-        let appr2 = evar_apprec ts env' evd [] c'2 in
-	evar_eqappr_x ts env' evd CONV appr1 appr2
+        eta env evd false term2 l2 term1 l1
 
     | Rigid c1, Rigid c2 -> begin
         match kind_of_term c1, kind_of_term c2 with
@@ -582,15 +596,21 @@ let choose_less_dependent_instance evk evd term args =
   if subst' = [] then evd, false else
   Evd.define evk (mkVar (fst (List.hd subst'))) evd, true
 
-let apply_on_subterm f c t =
+let apply_on_subterm evdref f c t =
   let rec applyrec (k,c as kc) t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
     if eq_constr c t then f k
     else
-      map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
-	applyrec kc t
+      match kind_of_term t with
+      | Evar (evk,args) when Evd.is_undefined !evdref evk ->
+          let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
+          let g (_,b,_) a = if b = None then applyrec kc a else a in
+          mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
+      | _ ->
+        map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
+	  applyrec kc t
   in
   applyrec (0,c) t
 
@@ -598,7 +618,8 @@ let filter_possible_projections c ty ctxt args =
   let fv1 = free_rels c in
   let fv2 = collect_vars c in
   let tyvars = collect_vars ty in
-  List.map2 (fun (id,_,_) a ->
+  List.map2 (fun (id,b,_) a ->
+    b <> None ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
@@ -670,7 +691,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
         ev in
-      set_holes evdref (apply_on_subterm set_var c rhs) subst
+      set_holes evdref (apply_on_subterm evdref set_var c rhs) subst
   | [] -> rhs in
 
   let subst = make_subst (ctxt,args,argoccs) in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 89ca95cb..d99b8c9f 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -178,12 +178,15 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
       | PApp (PApp (h, a1), a2), _ ->
           sorec stk subst (PApp(h,Array.append a1 a2)) t
 
-      | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
+      | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
           let p = Array.length args2 - Array.length args1 in
           if p>=0 then
             let args21, args22 = array_chop p args2 in
 	    let c = mkApp(c2,args21) in
-            let subst = merge_binding allow_bound_rels stk n c subst in
+            let subst =
+              match meta with
+              | None -> subst
+              | Some n -> merge_binding allow_bound_rels stk n c subst in
             array_fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3b679fce..3f6acfcb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -17,6 +17,19 @@ open Typeops
 open Declarations
 open Termops
 
+let get_type_from_constraints env sigma t =
+  if isEvar (fst (decompose_app t)) then
+    match
+      list_map_filter (fun (pbty,env,t1,t2) ->
+        if is_fconv Reduction.CONV env sigma t t1 then Some t2
+        else if is_fconv Reduction.CONV env sigma t t2 then Some t1
+        else None)
+        (snd (Evd.extract_all_conv_pbs sigma))
+    with
+    | t::l -> t
+    | _ -> raise Not_found
+  else raise Not_found
+ 
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
@@ -58,7 +71,12 @@ let retype ?(polyprop=true) sigma =
     | Construct cstr -> type_of_constructor env cstr
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
-          try Inductiveops.find_rectype env sigma (type_of env c)
+          let t = type_of env c in
+          try Inductiveops.find_rectype env sigma t
+          with Not_found ->
+          try
+            let t = get_type_from_constraints env sigma t in
+            Inductiveops.find_rectype env sigma t
           with Not_found -> anomaly "type_of: Bad recursive type" in
         let t = whd_beta sigma (applist (p, realargs)) in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index df5eff6a..fd045690 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -386,9 +386,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| Meta k, _
             when not (dependent cM cN) (* helps early trying alternatives *) ->
             if wt && flags.check_applied_meta_types then
-              (let tyM = Typing.meta_type sigma k in
-               let tyN = get_type_of curenv sigma cN in
-               check_compatibility curenv substn tyM tyN);
+              (try
+                 let tyM = Typing.meta_type sigma k in
+                 let tyN = get_type_of curenv sigma cN in
+                 check_compatibility curenv substn tyM tyN
+               with Anomaly _ (* Hack *) ->
+                 (* Renounce, maybe metas/evars prevents typing *) ());
 	    (* Here we check that [cN] does not contain any local variables *)
 	    if nb = 0 then
               sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
@@ -400,9 +403,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| _, Meta k
             when not (dependent cN cM) (* helps early trying alternatives *) ->
             if wt && flags.check_applied_meta_types then
-              (let tyM = get_type_of curenv sigma cM in
-               let tyN = Typing.meta_type sigma k in
-               check_compatibility curenv substn tyM tyN);
+              (try
+                 let tyM = get_type_of curenv sigma cM in
+                 let tyN = Typing.meta_type sigma k in
+                 check_compatibility curenv substn tyM tyN
+               with Anomaly _ (* Hack *) ->
+                 (* Renounce, maybe metas/evars prevents typing *) ());
 	    (* Here we check that [cM] does not contain any local variables *)
 	    if nb = 0 then
               (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst)