Fixing "change" and "fold" after convert_hyp/convert_concl moved to

new proof engine in e824d4293. Because of the expansion made by "fold"
and possibly by "change", checking the order of hypotheses is
necessary in general in "reduce". Before, it was done by side-effect
on reference "check", now it has to be explicit. To do for
optimization: flag each of the red_expr conversion strategy according
to whether they really need a check.

Also renamed the e_reduce family to e_change to emphasize that some
expansion can occur and that typing has to be rechecked.

This fixes recent failure of CoLoR (and probably Ergo).

2 files changed, 26 insertions, 26 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 08dbf39652..e9fbf6d156 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -119,13 +119,13 @@ let _ =
 let introduction    = Tacmach.introduction
 let refine          = Tacmach.refine
 
-let convert_concl ?(unsafe=false) ty k =
+let convert_concl ?(check=true) ty k =
   Proofview.Goal.nf_enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let conclty = Proofview.Goal.raw_concl gl in
     let sigma =
-      if not unsafe then begin
+      if check then begin
         ignore (Typing.type_of env sigma ty);
         let sigma,b = Reductionops.infer_conv env sigma ty conclty in
         if not b then error "Not convertible.";
@@ -138,18 +138,18 @@ let convert_concl ?(unsafe=false) ty k =
         (h, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
   end
 
-let convert_hyp ?(unsafe=false) d =
+let convert_hyp ?(check=true) d =
   Proofview.Goal.nf_enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let ty = Proofview.Goal.raw_concl gl in
-    let sign = convert_hyp (not unsafe) (named_context_val env) sigma d in
+    let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
     Proofview.Refine.refine (fun h -> Proofview.Refine.new_evar h ~main:true env ty)
   end
 
-let convert_concl_no_check = convert_concl ~unsafe:true
-let convert_hyp_no_check = convert_hyp ~unsafe:true
+let convert_concl_no_check = convert_concl ~check:false
+let convert_hyp_no_check = convert_hyp ~check:false
 
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
@@ -422,15 +422,15 @@ let bind_red_expr_occurrences occs nbcl redexp =
 let reduct_in_concl (redfun,sty) gl =
   Proofview.V82.of_tactic (convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty) gl
 
-let reduct_in_hyp redfun (id,where) gl =
-  Proofview.V82.of_tactic (convert_hyp_no_check
+let reduct_in_hyp ?(check=false) redfun (id,where) gl =
+  Proofview.V82.of_tactic (convert_hyp ~check
     (pf_reduce_decl redfun where (pf_get_hyp gl id) gl)) gl
 
 let revert_cast (redfun,kind as r) =
   if kind == DEFAULTcast then (redfun,REVERTcast) else r
 
-let reduct_option redfun = function
-  | Some id -> reduct_in_hyp (fst redfun) id
+let reduct_option ?(check=false) redfun = function
+  | Some id -> reduct_in_hyp ~check (fst redfun) id
   | None    -> reduct_in_concl (revert_cast redfun)
 
 (** Versions with evars to maintain the unification of universes resulting
@@ -440,12 +440,12 @@ let tclWITHEVARS f k gl =
   let evm, c' = pf_apply f gl in
     tclTHEN (tclEVARS evm) (k c') gl
 
-let e_reduct_in_concl (redfun,sty) gl =
+let e_change_in_concl (redfun,sty) gl =
   tclWITHEVARS
     (fun env sigma -> redfun env sigma (pf_concl gl))
     (fun c -> Proofview.V82.of_tactic (convert_concl_no_check c sty)) gl
 
-let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
+let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
   match c with
   | None ->
       if where == InHypValueOnly then
@@ -457,10 +457,10 @@ let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
       let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in
 	sigma', (id,Some b',ty')
 
-let e_reduct_in_hyp redfun (id,where) gl =
+let e_change_in_hyp redfun (id,where) gl =
   tclWITHEVARS
-    (e_pf_reduce_decl redfun where (pf_get_hyp gl id))
-    (fun s -> Proofview.V82.of_tactic (convert_hyp_no_check s)) gl
+    (e_pf_change_decl redfun where (pf_get_hyp gl id))
+    (fun s -> Proofview.V82.of_tactic (convert_hyp s)) gl
 
 type change_arg = env -> evar_map -> evar_map * constr
 
@@ -495,10 +495,10 @@ let change_on_subterm cv_pb deep t = function
       (fun subst -> change_and_check_subst Reduction.CONV subst t)
 
 let change_in_concl occl t =
-  e_reduct_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+  e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
 
 let change_in_hyp occl t id  =
-  with_check (e_reduct_in_hyp (fun x -> change_on_subterm Reduction.CONV x t occl) id)
+  e_change_in_hyp (fun x -> change_on_subterm Reduction.CONV x t occl) id
 
 let change_option occl t = function
   | Some id -> change_in_hyp occl t id
@@ -518,16 +518,16 @@ let change_concl t =
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
-let red_in_hyp          = reduct_in_hyp   red_product
+let red_in_hyp          = reduct_in_hyp    red_product
 let red_option          = reduct_option   (red_product,REVERTcast)
 let hnf_in_concl        = reduct_in_concl (hnf_constr,REVERTcast)
-let hnf_in_hyp          = reduct_in_hyp   hnf_constr
+let hnf_in_hyp          = reduct_in_hyp    hnf_constr
 let hnf_option          = reduct_option   (hnf_constr,REVERTcast)
 let simpl_in_concl      = reduct_in_concl (simpl,REVERTcast)
-let simpl_in_hyp        = reduct_in_hyp   simpl
+let simpl_in_hyp        = reduct_in_hyp    simpl
 let simpl_option        = reduct_option   (simpl,REVERTcast)
 let normalise_in_concl  = reduct_in_concl (compute,REVERTcast)
-let normalise_in_hyp    = reduct_in_hyp   compute
+let normalise_in_hyp    = reduct_in_hyp    compute
 let normalise_option    = reduct_option   (compute,REVERTcast)
 let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
 let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
@@ -549,7 +549,7 @@ let reduce redexp cl goal =
   let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
   let tac = tclMAP (fun (where,redexp) ->
-    reduct_option
+    reduct_option ~check:true
       (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
   match redexp with
   | Fold _ | Pattern _ -> with_check tac goal
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c2beefdfb8..e724f675e1 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -32,8 +32,8 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 
 val introduction    : Id.t -> tactic
 val refine          : constr -> tactic
-val convert_concl   : ?unsafe:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp     : ?unsafe:bool -> named_declaration -> unit Proofview.tactic
+val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
 val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
 val thin            : Id.t list -> tactic
@@ -127,8 +127,8 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 
 type change_arg = env -> evar_map -> evar_map * constr
 
-val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
-val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
+val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
+val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
 val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> tactic
 val change_concl      : constr -> tactic