diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-18 17:10:44 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-18 17:11:21 +0100 |
| commit | 0346ee4472711fc30b7cf197c1bad5c32140f831 (patch) | |
| tree | cf95696fc4acd3a8d64f9df9eb5b69cb0f5f8798 /plugins/funind/glob_term_to_relation.ml | |
| parent | 6f88442be8275361a7b68fd56d40976fdee9f4d5 (diff) | |
Fix a bug preventing the generation of graphs when doing multiple
pattern-matching on function calls.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 1b12cd42c..5d92fca5e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -681,7 +681,7 @@ and build_entry_lc_from_case env funname make_discr let case_resl = List.fold_right (fun (case_arg,_) ctxt_argsl -> - let arg_res = build_entry_lc env funname avoid case_arg in + let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in combine_results combine_args arg_res ctxt_argsl ) el |