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.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'plugins/firstorder/sequent.ml') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index fd5972fb7..98b178bde 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -253,17 +253,26 @@ let empty_seq depth= history=History.empty; depth=depth} -let create_with_ref_list l depth gl= +let expand_constructor_hints = + list_map_append (function + | IndRef ind -> + list_tabulate (fun i -> ConstructRef (ind,i+1)) + (Inductiveops.nconstructors ind) + | gr -> + [gr]) + +let extend_with_ref_list l seq gl= + let l = expand_constructor_hints l in let f gr seq= let c=constr_of_global gr in let typ=(pf_type_of gl c) in add_formula Hyp gr typ seq gl in - List.fold_right f l (empty_seq depth) + List.fold_right f l seq open Auto -let create_with_auto_hints l depth gl= - let seqref=ref (empty_seq depth) in +let extend_with_auto_hints l seq gl= + let seqref=ref seq in let f p_a_t = match p_a_t.code with Res_pf (c,_) | Give_exact c -- cgit v1.2.3