diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index fd5972fb74..98b178bdee 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 |