From dce9fe9bd4cab3e560f41a8d7cbf447b27665e1f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 13 Sep 2009 13:24:21 +0000 Subject: - Inductive types in the "using" option of auto/eauto/firstorder are interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/sequent.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/firstorder/sequent.mli') diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 51db9de16..206de27ed 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -57,10 +57,10 @@ val take_formula : t -> Formula.t * t val empty_seq : int -> t -val create_with_ref_list : global_reference list -> - int -> Proof_type.goal sigma -> t +val extend_with_ref_list : global_reference list -> + t -> Proof_type.goal sigma -> t -val create_with_auto_hints : Auto.hint_db_name list -> - int -> Proof_type.goal sigma -> t +val extend_with_auto_hints : Auto.hint_db_name list -> + t -> Proof_type.goal sigma -> t val print_cmap: global_reference list CM.t -> unit -- cgit v1.2.3