diff options
| author | Pierre-Marie Pédrot | 2016-11-12 01:28:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:47 +0100 |
| commit | 45562afa065aadc207dca4e904e309d835cb66ef (patch) | |
| tree | 2d7420427a49f17c2fb0d66ec8f38fe1df63abdb /tactics/elim.ml | |
| parent | 0489e8b56d7e10f7111c0171960e25d32201b963 (diff) | |
Tacticals API using EConstr.
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index bcb1c05cc9..fe36085b87 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -55,7 +55,7 @@ Another example : *) let elimHypThen tac id = - elimination_then tac (mkVar id) + elimination_then tac (EConstr.mkVar id) let rec general_decompose_on_hyp recognizer = ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) @@ -125,7 +125,7 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) let simple_elimination c = - elimination_then (fun _ -> tclIDTAC) c + elimination_then (fun _ -> tclIDTAC) (EConstr.of_constr c) let induction_trailer abs_i abs_j bargs = tclTHEN @@ -166,7 +166,7 @@ let double_ind h1 h2 = (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) (EConstr.mkVar id)))) end } let h_double_induction = double_ind |