Code cleaning & factorizing functions in Equality.

3 files changed, 26 insertions, 40 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5b73fbea2..6e50b923b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -138,15 +138,14 @@ let side_tac tac sidetac =
   | None -> tac
   | Some sidetac -> tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac
 
-let instantiate_lemma_all frzevars env gl c ty l l2r concl =
+let instantiate_lemma_all frzevars gl c ty l l2r concl =
+  let env = Proofview.Goal.env gl in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
-  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
-  let rec split_last_two = function
-      | [c1;c2] -> [],(c1, c2)
-      | x::y::z ->
-	  let l,res = split_last_two (y::z) in x::l, res
-      | _ -> error "The term provided is not an applied relation." in
-  let others,(c1,c2) = split_last_two args in
+  let (equiv, args) = decompose_appvect (Clenv.clenv_type eqclause) in
+  let arglen = Array.length args in
+  let () = if arglen < 2 then error "The term provided is not an applied relation." in
+  let c1 = args.(arglen - 2) in
+  let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
     clenv_pose_dependent_evars true {eqclause with evd = evd'}
   in
@@ -156,7 +155,7 @@ let instantiate_lemma_all frzevars env gl c ty l l2r concl =
       ((if l2r then c1 else c2),concl)
   in List.map try_occ occs
 
-let instantiate_lemma env gl c ty l l2r concl =
+let instantiate_lemma gl c ty l l2r concl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
@@ -191,20 +190,10 @@ let rewrite_conv_closed_unif_flags = {
   Unification.allow_K_in_toplevel_higher_order_unification = false
 }
 
-let rewrite_elim with_evars frzevars c e =
-  Proofview.Goal.raw_enter begin fun gl ->
-  let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
-  let elim gl = elimination_clause_scheme with_evars ~flags gl in
-  let tac gl = general_elim_clause_gen elim c e gl in
-  Proofview.V82.tactic tac
-  end
-
-let rewrite_elim_in with_evars frzevars id c e =
+let rewrite_elim with_evars frzevars cls c e =
   Proofview.Goal.raw_enter begin fun gl ->
   let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
-  let elim gl = elimination_in_clause_scheme with_evars ~flags id gl in
-  let tac gl = general_elim_clause_gen elim c e gl in
-  Proofview.V82.tactic tac
+  general_elim_clause with_evars flags cls c e
   end
 
 (* Ad hoc asymmetric general_elim_clause *)
@@ -216,8 +205,8 @@ let general_elim_clause with_evars frzevars cls rew elim =
       (* was tclWEAK_PROGRESS which only fails for tactics generating one
           subgoal and did not fail for useless conditional rewritings generating
           an extra condition *)
-      tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim)
-    | Some id -> rewrite_elim_in with_evars frzevars id rew elim
+      tclNOTSAMEGOAL (rewrite_elim with_evars frzevars cls rew elim)
+    | Some _ -> rewrite_elim with_evars frzevars cls rew elim
     end
     begin function
     | PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
@@ -241,10 +230,9 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
       tac
   in
   Proofview.Goal.raw_enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
     let instantiate_lemma concl =
-      if not all then instantiate_lemma env gl c t l l2r concl
-      else instantiate_lemma_all frzevars env gl c t l l2r concl
+      if not all then instantiate_lemma gl c t l l2r concl
+      else instantiate_lemma_all frzevars gl c t l l2r concl
     in
     let typ = match cls with
     | None -> pf_nf_concl gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 78d215ac8..00a35e236 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -839,15 +839,13 @@ let general_elim_clause_gen elimtac indclause elim gl =
     match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
   elimtac i (elimc, elimt, lbindelimc) indclause gl
 
-let general_elim_clause elimtac (c,lbindc) elim gl =
+let general_elim with_evars (c, lbindc) elim gl =
+  let elimtac = elimination_clause_scheme with_evars in
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let indclause  = pf_apply make_clenv_binding gl (c, t) lbindc in
   general_elim_clause_gen elimtac indclause elim gl
 
-let general_elim with_evars c e =
-  general_elim_clause (elimination_clause_scheme with_evars) c e
-
 (* Case analysis tactics *)
 
 let general_case_analysis_in_context with_evars (c,lbindc) gl =
@@ -958,6 +956,13 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, e
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id elimclause'' gl
 
+let general_elim_clause with_evars flags id c e =
+  let elim gl = match id with
+  | None -> elimination_clause_scheme with_evars ~flags gl
+  | Some id -> elimination_in_clause_scheme with_evars ~flags id gl
+  in
+  Proofview.V82.tactic (fun gl -> general_elim_clause_gen elim c e gl)
+
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
 type conjunction_status =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c3c799bae..81f63fc22 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -247,19 +247,12 @@ type eliminator = {
   elimbody : constr with_bindings
 }
 
-val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> 
-  int -> (constr * types * constr bindings) -> clausenv -> tactic
-
-val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> 
-  Id.t -> int -> (constr * types * constr bindings) -> clausenv -> tactic
-
-val general_elim_clause_gen :
-  (int -> (constr * types * constr bindings) -> 'a -> tactic) ->
-  'a -> eliminator -> tactic
-
 val general_elim  : evars_flag ->
   constr with_bindings -> eliminator -> tactic
 
+val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
+  clausenv -> eliminator -> unit Proofview.tactic
+
 val default_elim  : evars_flag -> constr with_bindings -> unit Proofview.tactic
 val simplest_elim : constr -> unit Proofview.tactic
 val elim :