Merge PR #10052: Cleanup the hypothesis conversion function

Reviewed-by: herbelin

4 files changed, 61 insertions, 61 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 70854e6e3c..0857c05968 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -514,7 +514,7 @@ let autounfold_one db cl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
+      | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
       | None -> convert_concl ~check:false c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3d760f1c3d..f049f8c568 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1613,10 +1613,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (tclTHENFIRST
     (tclTHENLIST [
-       (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
+       (change_in_hyp ~check:true None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+    (change_in_hyp ~check:true None (make_change_arg expected) (id,InHypTypeOnly)))
   end
 
 let try_rewrite tac =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e8869f9b0..806c955591 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -145,7 +145,7 @@ let introduction id =
 
 let error msg = CErrors.user_err Pp.(str msg)
 
-let convert_concl ?(check=true) ty k =
+let convert_concl ~check ty k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let conclty = Proofview.Goal.concl gl in
@@ -163,12 +163,12 @@ let convert_concl ?(check=true) ty k =
     end
   end
 
-let convert_hyp ?(check=true) d =
+let convert_hyp ~check ~reorder d =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let sign = convert_hyp check (named_context_val env) sigma d in
+    let sign = convert_hyp ~check ~reorder env sigma d in
     let env = reset_with_named_context sign env in
     Refine.refine ~typecheck:false begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ty
@@ -176,7 +176,7 @@ let convert_hyp ?(check=true) d =
   end
 
 let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false
+let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
 
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
@@ -701,7 +701,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
 
 (** Tactic reduction modulo evars (for universes essentially) *)
 
-let e_change_in_concl ?(check = false) (redfun, sty) =
+let e_change_in_concl ~check (redfun, sty) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
@@ -709,16 +709,16 @@ let e_change_in_concl ?(check = false) (redfun, sty) =
     (convert_concl ~check c' sty)
   end
 
-let e_change_in_hyp ?(check = false) redfun (id,where) =
+let e_change_in_hyp ~check ~reorder redfun (id,where) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let hyp = Tacmach.New.pf_get_hyp id gl in
     let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp ~check c)
+    (convert_hyp ~check ~reorder c)
   end
 
-let e_change_in_hyps ?(check=true) f args =
+let e_change_in_hyps ~check ~reorder f args =
   Proofview.Goal.enter begin fun gl ->
     let fold (env, sigma) arg =
       let (redfun, id, where) = f arg in
@@ -728,7 +728,7 @@ let e_change_in_hyps ?(check=true) f args =
           raise (RefinerError (env, sigma, NoSuchHyp id))
       in
       let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in
-      let sign = Logic.convert_hyp check (named_context_val env) sigma d in
+      let sign = Logic.convert_hyp ~check ~reorder env sigma d in
       let env = reset_with_named_context sign env in
       (env, sigma)
     in
@@ -745,26 +745,26 @@ let e_change_in_hyps ?(check=true) f args =
 
 let e_reduct_in_concl = e_change_in_concl
 
-let reduct_in_concl ?(check = false) (redfun, sty) =
+let reduct_in_concl ~check (redfun, sty) =
   let redfun env sigma c = (sigma, redfun env sigma c) in
   e_change_in_concl ~check (redfun, sty)
 
-let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+let e_reduct_in_hyp ~check ~reorder redfun (id, where) =
   let redfun _ env sigma c = redfun env sigma c in
-  e_change_in_hyp ~check redfun (id, where)
+  e_change_in_hyp ~check ~reorder redfun (id, where)
 
-let reduct_in_hyp ?(check = false) redfun (id, where) =
+let reduct_in_hyp ~check ~reorder redfun (id, where) =
   let redfun _ env sigma c = (sigma, redfun env sigma c) in
-  e_change_in_hyp ~check redfun (id, where)
+  e_change_in_hyp ~check ~reorder redfun (id, where)
 
 let revert_cast (redfun,kind as r) =
   if kind == DEFAULTcast then (redfun,REVERTcast) else r
 
-let e_reduct_option ?(check=false) redfun = function
-  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
+let e_reduct_option ~check redfun = function
+  | Some id -> e_reduct_in_hyp ~check ~reorder:check (fst redfun) id
   | None    -> e_change_in_concl ~check (revert_cast redfun)
 
-let reduct_option ?(check = false) (redfun, sty) where =
+let reduct_option ~check (redfun, sty) where =
   let redfun env sigma c = (sigma, redfun env sigma c) in
   e_reduct_option ~check (redfun, sty) where
 
@@ -802,7 +802,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   | Some sigma -> (sigma, t')
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm check cv_pb deep t where env sigma c =
+let change_on_subterm ~check cv_pb deep t where env sigma c =
   let mayneedglobalcheck = ref false in
   let (sigma, c) = match where with
   | None ->
@@ -825,15 +825,13 @@ let change_on_subterm check cv_pb deep t where env sigma c =
     end;
   (sigma, c)
 
-let change_in_concl ?(check=true) occl t =
+let change_in_concl ~check occl t =
   (* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
-  e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast)
+  e_change_in_concl ~check:false ((change_on_subterm ~check Reduction.CUMUL false t occl),DEFAULTcast)
 
-let change_in_hyp ?(check=true) occl t id =
-  (* FIXME: we set the [check] flag only to reorder hypotheses in case of
-    introduction of dependencies in new variables. We should separate this
-    check from the conversion function. *)
-  e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id
+let change_in_hyp ~check occl t id  =
+  (* Same as above *)
+  e_change_in_hyp ~check:false ~reorder:check (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id
 
 let concrete_clause_of enum_hyps cl = match cl.onhyps with
 | None ->
@@ -842,7 +840,7 @@ let concrete_clause_of enum_hyps cl = match cl.onhyps with
 | Some l ->
   List.map (fun ((occs, id), w) -> (id, occs, w)) l
 
-let change ?(check=true) chg c cls =
+let change ~check chg c cls =
   Proofview.Goal.enter begin fun gl ->
     let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
     begin match cls.concl_occs with
@@ -852,33 +850,34 @@ let change ?(check=true) chg c cls =
     <*>
     let f (id, occs, where) =
       let occl = bind_change_occurrences occs chg in
-      let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in
+      let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in
       (redfun, id, where)
     in
-    e_change_in_hyps ~check f hyps
+    (* Don't check, we do it already in [change_on_subterm] *)
+    e_change_in_hyps ~check:false ~reorder:check f hyps
   end
 
 let change_concl t = 
   change_in_concl ~check:true None (make_change_arg 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_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_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_option        = reduct_option   (simpl,REVERTcast)
-let normalise_in_concl  = reduct_in_concl (compute,REVERTcast)
-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)
-let unfold_in_hyp   loccname = reduct_in_hyp   (unfoldn loccname)
-let unfold_option   loccname = reduct_option (unfoldn loccname,DEFAULTcast)
-let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
+let red_in_concl        = reduct_in_concl ~check:false (red_product,REVERTcast)
+let red_in_hyp          = reduct_in_hyp ~check:false ~reorder:false red_product
+let red_option          = reduct_option ~check:false (red_product,REVERTcast)
+let hnf_in_concl        = reduct_in_concl ~check:false (hnf_constr,REVERTcast)
+let hnf_in_hyp          = reduct_in_hyp ~check:false ~reorder:false hnf_constr
+let hnf_option          = reduct_option ~check:false (hnf_constr,REVERTcast)
+let simpl_in_concl      = reduct_in_concl ~check:false (simpl,REVERTcast)
+let simpl_in_hyp        = reduct_in_hyp ~check:false ~reorder:false simpl
+let simpl_option        = reduct_option ~check:false (simpl,REVERTcast)
+let normalise_in_concl  = reduct_in_concl ~check:false (compute,REVERTcast)
+let normalise_in_hyp    = reduct_in_hyp ~check:false ~reorder:false compute
+let normalise_option    = reduct_option ~check:false (compute,REVERTcast)
+let normalise_vm_in_concl = reduct_in_concl ~check:false (Redexpr.cbv_vm,VMcast)
+let unfold_in_concl loccname = reduct_in_concl ~check:false (unfoldn loccname,REVERTcast)
+let unfold_in_hyp   loccname = reduct_in_hyp ~check:false ~reorder:false (unfoldn loccname)
+let unfold_option   loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast)
+let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast)
 
 (* The main reduction function *)
 
@@ -893,6 +892,7 @@ let reduce redexp cl =
   let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
   let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
+  let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   begin match cl.concl_occs with
   | NoOccurrences -> Proofview.tclUNIT ()
   | occs ->
@@ -907,7 +907,7 @@ let reduce redexp cl =
     let redfun _ env sigma c = redfun env sigma c in
     (redfun, id, where)
   in
-  e_change_in_hyps ~check f hyps
+  e_change_in_hyps ~check ~reorder f hyps
   end
   end
 
@@ -2654,7 +2654,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
       [ Proofview.Unsafe.tclEVARS sigma;
         convert_concl ~check:false newcl DEFAULTcast;
         intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false;
-        Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls;
+        Tacticals.New.tclMAP (convert_hyp ~check:false ~reorder:false) depdecls;
         eq_tac ]
   end
 
@@ -3061,8 +3061,8 @@ let unfold_body x =
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
   let rfun _ _ c = replace_vars [x, xval] c in
-  let reducth h = reduct_in_hyp rfun h in
-  let reductc = reduct_in_concl (rfun, DEFAULTcast) in
+  let reducth h = reduct_in_hyp ~check:false ~reorder:false rfun h in
+  let reductc = reduct_in_concl ~check:false (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
   end
   end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b3914816ac..9eb8196280 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -33,8 +33,8 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 (** {6 Primitive tactics. } *)
 
 val introduction    : Id.t -> 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   : check:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp     : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
 [@@ocaml.deprecated "use [Tactics.convert_concl]"]
 val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
@@ -152,13 +152,13 @@ type e_tactic_reduction = Reductionops.e_reduction_function
 type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
 
 val make_change_arg   : constr -> change_arg
-val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
-val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
-val reduct_in_concl   : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
-val change_in_concl   : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val reduct_in_hyp     : check:bool -> reorder:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
+val reduct_option     : check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
+val reduct_in_concl   : check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
+val e_reduct_in_concl   : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val change_in_concl   : check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
 val change_concl      : constr -> unit Proofview.tactic
-val change_in_hyp     : ?check:bool -> (occurrences * constr_pattern) option -> change_arg ->
+val change_in_hyp     : check:bool -> (occurrences * constr_pattern) option -> change_arg ->
                         hyp_location -> unit Proofview.tactic
 val red_in_concl      : unit Proofview.tactic
 val red_in_hyp        : hyp_location -> unit Proofview.tactic
@@ -180,7 +180,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
 val change            :
-  ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
+  check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> unit Proofview.tactic
 val reduce            : red_expr -> clause -> unit Proofview.tactic