Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

7 files changed, 90 insertions, 56 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1819dc52..38355cf1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1763,7 +1763,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Second strategy: we directly use the evar as a non dependent pred *)
-        let pred2 = lift (List.length arsign) t in
+        let pred2 = lift (List.length (List.flatten arsign)) t in
 	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
     | Some rtntyp, _ ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 69ff2af9..a74e4cb4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -389,6 +389,8 @@ let rec detype (isgoal:bool) avoid env t =
 	 with _ ->
 	  GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
+    | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
+        detype isgoal avoid env c1
     | Cast (c1,k,c2) ->
 	GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fa29243a..b0248a84 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -135,15 +135,20 @@ let whd_head_evar_stack sigma c =
 
 let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
-let noccur_evar evd evk c =
-  let rec occur_rec c = match kind_of_term c with
-  | Evar (evk',_ as ev') ->
+let noccur_evar env evd evk c =
+  let rec occur_rec k c = match kind_of_term c with
+  | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec c
-       | None -> if evk = evk' then raise Occur)
-  | _ -> iter_constr occur_rec c
+       | Some c -> occur_rec k c
+       | None ->
+           if evk = evk' then raise Occur else Array.iter (occur_rec k) args')
+  | Rel i when i > k ->
+      (match pi2 (Environ.lookup_rel (i-k) env) with
+       | None -> ()
+       | Some b -> occur_rec k (lift i b))
+  | _ -> iter_constr_with_binders succ occur_rec k c
   in
-  try occur_rec c; true with Occur -> false
+  try occur_rec 0 c; true with Occur -> false
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -741,7 +746,8 @@ let is_unification_pattern_meta env nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then
+  if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
+  then
     let args = remove_instance_local_defs evd evk (Array.to_list args) in
     let n = List.length args in
     match find_unification_pattern_args env (args @ l) t with
@@ -1112,10 +1118,11 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
     | Not_found -> CannotInvert
     | NotUnique -> Invertible NoUniqueProjection
 
-let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
+let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
   let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
   match res with
-  | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) ->
+  | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
+      ->
       CannotInvert
   | _ ->
       res
@@ -1153,10 +1160,11 @@ let extract_candidates sols =
 
 let filter_of_projection = function Invertible _ -> true | _ -> false
 
-let invert_invertible_arg evd aliases k (evk,argsv) args' =
+let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
   let evi = Evd.find_undefined evd evk in
   let subst,_ = make_projectable_subst aliases evd evi argsv in
-  let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in
+  let projs =
+    array_map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
   Array.of_list (extract_unique_projections projs)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -1364,12 +1372,14 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
 
 let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
   let filter1 =
-    restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1)
+    restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
+      (Array.to_list argsv1)
   in
   let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
   let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
   let filter2 =
-    restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2)
+    restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
+      (Array.to_list argsv2)
   in
   let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
   let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
@@ -1389,7 +1399,7 @@ let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2
     try
       let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
       let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
-      evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1)
+      evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
     with
     | EvarSolvedWhileRestricting (evd,ev1) ->
         raise (EvarSolvedOnTheFly (evd,ev1))
@@ -1585,7 +1595,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,Array.map (lift k) argsv) in
-          let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev'  ev in
+          let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev'  ev in
 	  evdref := evd;
           body
         with
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 24c5ba5b..8e4b211f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -346,8 +346,38 @@ let rec cases_pattern_of_glob_constr na = function
   | GHole (loc,_) -> PatVar (loc,na)
   | GRef (loc,ConstructRef cstr) ->
       PatCstr (loc,cstr,[],na)
-  | GApp (loc,GRef (_,ConstructRef cstr),l) ->
-      PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+  | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
+      let mib,_ = Global.lookup_inductive ind in
+      let nparams = mib.Declarations.mind_nparams in
+      if nparams > List.length args then
+        user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
+      let params,args = list_chop nparams args in
+      List.iter (function GHole _ -> ()
+	| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
+        params;
+      let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
+      PatCstr (loc,cstr,args,na)
+  | _ -> raise Not_found
+
+let rec cases_pattern_of_glob_constr na = function
+  | GVar (loc,id) when na<>Anonymous ->
+      (* Unable to manage the presence of both an alias and a variable *)
+      raise Not_found
+  | GVar (loc,id) -> PatVar (loc,Name id)
+  | GHole (loc,_) -> PatVar (loc,na)
+  | GRef (loc,ConstructRef cstr) ->
+      PatCstr (loc,cstr,[],na)
+  | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
+      let mib,_ = Global.lookup_inductive ind in
+      let nparams = mib.Declarations.mind_nparams in
+      if nparams > List.length args then
+        user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
+      let params,args = list_chop nparams args in
+      List.iter (function GHole _ -> ()
+	| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
+        params;
+      let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
+      PatCstr (loc,cstr,args,na)
   | _ -> raise Not_found
 
 (* Turn a closed cases pattern into a glob_constr *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 665491e7..22aacb29 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -42,6 +42,11 @@ let e_type_judgment env evdref j =
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type env j
 
+let e_assumption_of_judgment env evdref j =
+  try (e_type_judgment env evdref j).utj_val
+  with TypeError _ ->
+    error_assumption env j
+
 let e_judge_of_apply env evdref funj argjv =
   let rec apply_rec n typ = function
   | [] ->
@@ -150,7 +155,7 @@ let rec execute env evdref cstr =
     | Evar ev ->
 	let ty = Evd.existential_type !evdref ev in
 	let jty = execute env evdref (whd_evar !evdref ty) in
-	let jty = assumption_of_judgment env jty in
+	let jty = e_assumption_of_judgment env evdref jty in
 	{ uj_val = cstr; uj_type = jty }
 
     | Rel n ->
@@ -243,7 +248,7 @@ let rec execute env evdref cstr =
 
 and execute_recdef env evdref (names,lar,vdef) =
   let larj = execute_array env evdref lar in
-  let lara = Array.map (assumption_of_judgment env) larj in
+  let lara = Array.map (e_assumption_of_judgment env evdref) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
   let vdefv = Array.map j_val vdefj in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c92c183d..63cdb378 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -198,11 +198,18 @@ type unify_flags = {
     (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
 
   modulo_delta : Names.transparent_state;
-    (* This controls which constant are unfoldable; this is on for apply *)
+    (* This controls which constants are unfoldable; this is on for apply *)
     (* (but not simple apply) since Feb 2008 for 8.2 *)
 
   modulo_delta_types : Names.transparent_state;
 
+  modulo_delta_in_merge : Names.transparent_state option;
+    (* This controls whether unfoldability is different when trying to unify *)
+    (* several instances of the same metavariable *)
+    (* Typical situation is when we give a pattern to be matched *)
+    (* syntactically against a subterm but we want the metas of the *)
+    (* pattern to be modulo convertibility *)
+
   check_applied_meta_types : bool;
     (* This controls whether meta's applied to arguments have their *)
     (* type unified with the type of their instance *)
@@ -240,12 +247,13 @@ type unify_flags = {
 }
 
 (* Default flag for unifying a type against a type (e.g. apply) *)
-(* We set all conversion flags *)
+(* We set all conversion flags (no flag should be modified anymore) *)
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = full_transparent_state;
   modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = None;
   check_applied_meta_types = true;
   resolve_evars = false;
   use_pattern_unification = true;
@@ -258,24 +266,22 @@ let default_unify_flags = {
       (* in fact useless when not used in w_unify_to_subterm_list *)
 }
 
+let set_merge_flags flags =
+  match flags.modulo_delta_in_merge with
+  | None -> flags
+  | Some ts ->
+    { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts }
+
 (* Default flag for the "simple apply" version of unification of a *)
 (* type against a type (e.g. apply) *)
 (* We set only the flags available at the time the new "apply" extends *)
 (* out of "simple apply" *)
-let default_no_delta_unify_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = true;
+let default_no_delta_unify_flags = { default_unify_flags with
   modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
-  restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
-  modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
 }
 
 (* Default flags for looking for subterms in elimination tactics *)
@@ -283,36 +289,16 @@ let default_no_delta_unify_flags = {
 (* allow_K) because only closed terms are involved in *)
 (* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
 (* call w_unify for induction/destruct/case/elim  (13/6/2011) *)
-let elim_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = true;
-  modulo_delta = full_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  check_applied_meta_types = true;
-  resolve_evars = false;
-  use_pattern_unification = true;
-  use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
+let elim_flags = { default_unify_flags with
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
-  modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = true
 }
 
-let elim_no_delta_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = true;
+let elim_no_delta_flags = { elim_flags with
   modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = false;
-  use_meta_bound_pattern_unification = true;
-  frozen_evars = ExistentialSet.empty;
-  restrict_conv_on_strict_subterms = false; (* ? *)
-  modulo_betaiota = false;
-  modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = true
 }
 
 let set_no_head_reduction flags =
@@ -865,7 +851,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	if Evd.is_defined evd evk then
 	  let v = Evd.existential_value evd ev in
 	  let (evd,metas',evars'') =
-	    unify_0 curenv evd CONV flags rhs v in
+	    unify_0 curenv evd CONV (set_merge_flags flags) rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
 	  (* This can make rhs' ill-typed if metas are *)
@@ -943,7 +929,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
-      unify_0 sp_env evd' CUMUL flags
+      unify_0 sp_env evd' CUMUL (set_merge_flags flags)
         (get_type_of sp_env evd' c) ev.evar_concl in
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e3fd46af..1ec5c1a2 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,6 +15,7 @@ type unify_flags = {
   use_metas_eagerly_in_conv_on_closed_terms : bool;
   modulo_delta : Names.transparent_state;
   modulo_delta_types : Names.transparent_state;
+  modulo_delta_in_merge : Names.transparent_state option;
   check_applied_meta_types : bool;
   resolve_evars : bool;
   use_pattern_unification : bool;