Ensured that the transparency state is used when flag betaiota is on for apply.

+ small typo fix in r14217
+ added compatibility of betaiota flag with 8.3 when "-compat 8.3" is given

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 58 insertions, 41 deletions

diff --git a/CHANGES b/CHANGES
index 90d8b604f1..54b44309e8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,7 +35,7 @@ Tactics
 - Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
 - Unification in "apply" supports unification of patterns of the form
   ?f x y = g(x,y) (compatibility ensured by using
-  "Unset Tactic Pattern Unification").
+  "Unset Tactic Pattern Unification"). It also supports (full) betaiota.
 - Tactic autorewrite does no longer instantiate pre-existing
   existential variables (theoretical source of possible incompatibility).
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 196adaae5f..32a0b2ac55 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -55,19 +55,19 @@ let eval_flexible_term ts env c =
   | Lambda _ -> Some c
   | _ -> assert false
 
-let evar_apprec env evd stack c =
+let evar_apprec ts env evd stack c =
   let sigma =  evd in
   let rec aux s =
-    let (t,stack) = whd_betaiota_deltazeta_for_iota_state env sigma s in
+    let (t,stack) = whd_betaiota_deltazeta_for_iota_state ts env sigma s in
     match kind_of_term t with
       | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
 	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack_list stack empty_stack)
 
-let apprec_nohdbeta env evd c =
+let apprec_nohdbeta ts env evd c =
   match kind_of_term (fst (Reductionops.whd_stack evd c)) with
-    | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
+    | (Case _ | Fix _) -> applist (evar_apprec ts env evd [] c)
     | _ -> c
 
 let position_problem l2r = function
@@ -183,8 +183,8 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
-        let term1 = apprec_nohdbeta env evd term1 in
-        let term2 = apprec_nohdbeta env evd term2 in
+        let term1 = apprec_nohdbeta ts env evd term1 in
+        let term2 = apprec_nohdbeta ts env evd term2 in
         if is_undefined_evar evd term1 then
           solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,destEvar term1,term2)
@@ -253,7 +253,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	and f2 i =
 	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None -> (i,false)
 	in
 	ise_try evd [f1; f2]
@@ -285,7 +285,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	and f2 i =
 	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None -> (i,false)
 	in
 	ise_try evd [f1; f2]
@@ -302,8 +302,8 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
 	     (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)]
 	and f2 i =
-          let appr1 = evar_apprec env i l1 (subst1 b1 c'1)
-          and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
+          let appr1 = evar_apprec ts env i l1 (subst1 b1 c'1)
+          and appr2 = evar_apprec ts env i l2 (subst1 b2 c'2)
 	  in evar_eqappr_x ts env i pbty appr1 appr2
 	in
 	ise_try evd [f1; f2]
@@ -328,20 +328,20 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None ->
 		match eval_flexible_term ts env flex2 with
 		| Some v2 ->
-		    evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
+		    evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 		| None -> (i,false)
 	  else
 	    match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None ->
 		match eval_flexible_term ts env flex1 with
 		| Some v1 ->
-		    evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
+		    evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 		| None -> (i,false)
 	in
 	ise_try evd [f1; f2; f3]
@@ -396,7 +396,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	and f4 i =
 	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
- 		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
@@ -408,7 +408,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	and f4 i =
 	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
- 		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
@@ -419,7 +419,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	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 env' evd [] c'1 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
 
@@ -429,7 +429,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
         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 env' evd [] c'2 in
+        let appr2 = evar_apprec ts env' evd [] c'2 in
 	evar_eqappr_x ts env' evd CONV appr1 appr2
 
     | Rigid c1, Rigid c2 -> begin
@@ -568,8 +568,8 @@ let choose_less_dependent_instance evk evd term args =
   Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
-  let t1 = apprec_nohdbeta env evd (whd_head_evar evd t1) in
-  let t2 = apprec_nohdbeta env evd (whd_head_evar evd t2) in
+  let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
+  let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 92ad6bea66..2762a52a16 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -292,7 +292,7 @@ let reduce_fix whdfun sigma fix stack =
                               -------------------
    qui coute cher *)
 
-let rec whd_state_gen flags env sigma =
+let rec whd_state_gen flags ts env sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | Rel n when red_delta flags ->
@@ -311,7 +311,7 @@ let rec whd_state_gen flags env sigma =
 	  (match safe_meta_value sigma ev with
 	     | Some body -> whrec (body, stack)
 	     | None -> s)
-      | Const const when red_delta flags ->
+      | Const const when is_transparent_constant ts const ->
 	  (match constant_opt_value env const with
 	     | Some  body -> whrec (body, stack)
 	     | None -> s)
@@ -323,7 +323,7 @@ let rec whd_state_gen flags env sigma =
              | Some (a,m) when red_beta flags -> stacklam whrec [a] c m
              | None when red_eta flags ->
 		 let env' = push_rel (na,None,t) env in
-		 let whrec' = whd_state_gen flags env' sigma in
+		 let whrec' = whd_state_gen flags ts env' sigma in
                  (match kind_of_term (app_stack (whrec' (c, empty_stack))) with
                     | App (f,cl) ->
 			let napp = Array.length cl in
@@ -434,18 +434,19 @@ let whd_betalet = red_of_state_red whd_betalet_state
 
 (* 2. Delta Reduction Functions *)
 
-let whd_delta_state e = whd_state_gen delta e
+let whd_delta_state e = whd_state_gen delta full_transparent_state e
 let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
 let whd_delta env = red_of_state_red  (whd_delta_state env)
 
-let whd_betadelta_state e = whd_state_gen betadelta e
+let whd_betadelta_state e = whd_state_gen betadelta full_transparent_state e
 let whd_betadelta_stack env =
   stack_red_of_state_red (whd_betadelta_state env)
 let whd_betadelta env =
   red_of_state_red (whd_betadelta_state env)
 
 
-let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
+let whd_betadeltaeta_state e =
+  whd_state_gen betadeltaeta full_transparent_state e
 let whd_betadeltaeta_stack env =
   stack_red_of_state_red (whd_betadeltaeta_state env)
 let whd_betadeltaeta env =
@@ -461,19 +462,29 @@ let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
 let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
 let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
-let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
+let whd_betadeltaiota_state env =
+  whd_state_gen betadeltaiota full_transparent_state env
 let whd_betadeltaiota_stack env =
   stack_red_of_state_red (whd_betadeltaiota_state env)
 let whd_betadeltaiota env =
   red_of_state_red (whd_betadeltaiota_state env)
 
-let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
+let whd_betadeltaiota_state_using ts env =
+  whd_state_gen betadeltaiota ts env
+let whd_betadeltaiota_stack_using ts env =
+  stack_red_of_state_red (whd_betadeltaiota_state_using ts env)
+let whd_betadeltaiota_using ts env =
+  red_of_state_red (whd_betadeltaiota_state_using ts env)
+
+let whd_betadeltaiotaeta_state env =
+  whd_state_gen betadeltaiotaeta full_transparent_state env
 let whd_betadeltaiotaeta_stack env =
   stack_red_of_state_red (whd_betadeltaiotaeta_state env)
 let whd_betadeltaiotaeta env =
   red_of_state_red (whd_betadeltaiotaeta_state env)
 
-let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
+let whd_betadeltaiota_nolet_state env =
+  whd_state_gen betadeltaiota_nolet full_transparent_state env
 let whd_betadeltaiota_nolet_stack env =
   stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
 let whd_betadeltaiota_nolet env =
@@ -795,19 +806,21 @@ let is_sort env sigma arity =
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
 
-let whd_betaiota_deltazeta_for_iota_state env sigma s =
+let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
   let rec whrec s =
     let (t, stack as s) = whd_betaiota_state sigma s in
     match kind_of_term t with
     | Case (ci,p,d,lf) ->
-        let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
+        let (cr,crargs) = whd_betadeltaiota_stack_using ts env sigma d in
         let rslt = mkCase (ci, p, applist (cr,crargs), lf) in
         if reducible_mind_case cr then
 	  whrec (rslt, stack)
         else
 	  s
     | Fix fix ->
-	  (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
+	  (match
+              reduce_fix (whd_betadeltaiota_state_using ts env) sigma fix stack
+           with
              | Reduced s -> whrec s
 	     | NotReducible -> s)
     | _ -> s
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d6d97179e7..1a90b23f21 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -213,7 +213,8 @@ val head_unfold_under_prod : transparent_state -> reduction_function
 
 (** {6 Heuristic for Conversion with Evar } *)
 
-val whd_betaiota_deltazeta_for_iota_state :  state_reduction_function
+val whd_betaiota_deltazeta_for_iota_state :
+  transparent_state -> state_reduction_function
 
 (** {6 Meta-related reduction functions } *)
 val meta_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 79debed864..d90ea6fc93 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -223,7 +223,7 @@ let default_unify_flags = {
   use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = true;
+  modulo_betaiota = false;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
       (* in fact useless when not used in w_unify_to_subterm_list *)
@@ -327,10 +327,13 @@ let oracle_order env cf1 cf2 =
       | None -> Some true
       | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
 
-let do_reduce env sigma c =
-  let (t, l) = whd_betaiota_deltazeta_for_iota_state env sigma (c, empty_stack) in
+let do_reduce ts env sigma c =
+  let (t, l) = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in
     applist (t, list_of_stack l)
 
+let use_full_betaiota flags =
+  flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
+
 let isAllowedEvar flags c = match kind_of_term c with
   | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars)
   | _ -> false
@@ -453,12 +456,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		    expand curenvnb pb b substn cM f1 l1 cN f2 l2
 
   and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN =
-    if flags.modulo_betaiota && not (subterm_restriction b flags) then
-      let cM' = do_reduce (fst curenvnb) sigma cM in
+    if use_full_betaiota flags && not (subterm_restriction b flags) then
+      let cM' = do_reduce flags.modulo_delta (fst curenvnb) sigma cM in
 	if not (eq_constr cM cM') then
 	  unirec_rec curenvnb pb b substn cM' cN
 	else
-	  let cN' = do_reduce (fst curenvnb) sigma cN in
+	  let cN' = do_reduce flags.modulo_delta (fst curenvnb) sigma cN in
 	    if not (eq_constr cN cN') then
 	      unirec_rec curenvnb pb b substn cM cN'
 	    else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -925,7 +928,7 @@ let w_typed_unify_list env flags f1 l1 f2 l2 evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let subst =
     List.fold_left2 (fun subst m n ->
-      unify_0_with_initial_metas subst true env CONV flags' m n) (evd,[],[])
+      unify_0_with_initial_metas subst true env CONV flags' m n) (evd',[],[])
       (f1::l1) (f2::l2) in
   let evd = w_merge env true flags subst in
   try_resolve_typeclasses env evd flags (applist(f1,l1)) (applist(f2,l2))