diff options
Diffstat (limited to 'plugins/firstorder/rules.mli')
| -rw-r--r-- | plugins/firstorder/rules.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index bfebbaaf88..180f6f5da1 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -33,19 +33,19 @@ val or_tac : seqtac with_backtracking val arrow_tac : seqtac with_backtracking -val left_and_tac : inductive -> lseqtac with_backtracking +val left_and_tac : pinductive -> lseqtac with_backtracking -val left_or_tac : inductive -> lseqtac with_backtracking +val left_or_tac : pinductive -> lseqtac with_backtracking val left_false_tac : global_reference -> tactic -val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking +val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking val forall_tac : seqtac with_backtracking -val left_exists_tac : inductive -> lseqtac with_backtracking +val left_exists_tac : pinductive -> lseqtac with_backtracking val ll_forall_tac : types -> lseqtac with_backtracking |