Use a dedicated type for equality elimination.

In this mess of higher-order callbacks it helps sorting out the invariants
of the structure.

1 files changed, 21 insertions, 11 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index b4def7bb51..ecc9436db6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1013,6 +1013,10 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
     Proofview.tclUNIT
        (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
 
+type equality = {
+  eq_data  : (coq_eq_data * EConstr.t * (EConstr.t * EConstr.t * EConstr.t));
+  eq_clenv : clausenv;
+}
 
 let eq_baseid = Id.of_string "e"
 
@@ -1025,7 +1029,7 @@ let apply_on_clause (f,t) clause =
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
 
-let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
+let discr_positions env sigma { eq_data = (lbeq,eqn,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn =
   build_coq_True () >>= fun true_0 ->
   build_coq_False () >>= fun false_0 ->
   let false_ty = Retyping.get_type_of env sigma false_0 in
@@ -1049,7 +1053,8 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
     tclTHENS (assert_after Anonymous false_0)
       [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
 
-let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
+let discrEq eq =
+  let { eq_data = (_, _, (_, t1, t2)); eq_clenv = eq_clause } = eq in
   let sigma = eq_clause.evd in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -1058,7 +1063,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
       let info = Exninfo.reify () in
       tclZEROMSG ~info (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
-      discr_positions env sigma u eq_clause cpath dirn
+      discr_positions env sigma eq cpath dirn
   end
 
 let onEquality with_evars tac (c,lbindc) =
@@ -1071,9 +1076,10 @@ let onEquality with_evars tac (c,lbindc) =
   let eqn = clenv_type eq_clause' in
   (* FIXME evar leak *)
   let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in
+  let eq = { eq_data = (eq,eqn,eq_args); eq_clenv = eq_clause' } in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
-    (tac (eq,eqn,eq_args) eq_clause')
+    (tac eq)
   end
 
 let onNegatedEquality with_evars tac =
@@ -1385,7 +1391,8 @@ let simplify_args env sigma t =
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
+let inject_at_positions env sigma l2r eq posns tac =
+  let { eq_data = (eq,_,(t,t1,t2)); eq_clenv = eq_clause } = eq in
   let e = next_ident_away eq_baseid (vars_of_env env) in
   let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in
   let evdref = ref sigma in
@@ -1422,7 +1429,8 @@ let () = CErrors.register_handler (function
   | NothingToInject -> Some (Pp.str "Nothing to inject.")
   | _ -> None)
 
-let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let injEqThen keep_proofs tac l2r eql =
+  let { eq_data = (eq,_,(t,t1,t2)); eq_clenv = eq_clause } = eql in
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with
@@ -1437,7 +1445,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   | Inr [([],_,_)] ->
      Proofview.tclZERO NothingToInject
   | Inr posns ->
-      inject_at_positions env sigma l2r u eq_clause posns
+      inject_at_positions env sigma l2r eql posns
         (tac (clenv_value eq_clause))
 
 let get_previous_hyp_position id gl =
@@ -1491,17 +1499,18 @@ let simpleInjClause flags with_evars = function
 let injConcl flags = injClause flags None false None
 let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id)))
 
-let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
+let decompEqThen keep_proofs ntac eq =
+  let { eq_data = (_,_,(_,t1,t2) as u); eq_clenv = clause } = eq in
   Proofview.Goal.enter begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
-          discr_positions env sigma u clause cpath dirn
+          discr_positions env sigma eq cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
         ntac (clenv_value clause) 0
     | Inr posns ->
-        inject_at_positions env sigma true u clause posns
+        inject_at_positions env sigma true eq posns
           (ntac (clenv_value clause))
   end
 
@@ -1516,7 +1525,8 @@ let dEq ~keep_proofs with_evars =
 let intro_decomp_eq tac data (c, t) =
   Proofview.Goal.enter begin fun gl ->
     let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
-    decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl
+    let eq = { eq_data = data; eq_clenv = cl } in
+    decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq
   end
 
 let () = declare_intro_decomp_eq intro_decomp_eq