diff options
| author | Pierre-Marie Pédrot | 2016-05-13 00:16:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 21:17:24 +0200 |
| commit | 73cdb000ec07ec484557839c4b94fcf779df2f06 (patch) | |
| tree | 4aa04d713d26b537c187e1be801b4788d4a4e915 /plugins/firstorder | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
Put the "clear" tactic into the monad.
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/rules.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index c05015c538..f19cdd2ccc 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -52,7 +52,7 @@ let basename_of_global=function | _->assert false let clear_global=function - VarRef id->clear [id] + VarRef id-> Proofview.V82.of_tactic (clear [id]) | _->tclIDTAC (* connection rules *) @@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq= (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (clear [id0]) gls)); + tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; |