From 0346ee4472711fc30b7cf197c1bad5c32140f831 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 18 Nov 2015 17:10:44 +0100 Subject: Fix a bug preventing the generation of graphs when doing multiple pattern-matching on function calls. --- plugins/funind/glob_term_to_relation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 1b12cd42ce..5d92fca5ea 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 -- cgit v1.2.3 From 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 19 Nov 2015 17:48:32 +0100 Subject: Fix bug #4433, removing hack on evars appearing in a pattern from a constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore. --- plugins/quote/quote.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 2a2ef30fb1..b72ebbc927 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f = let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> - PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args) + PApp (pattern_of_constr (Global.env()) Evd.empty f, Array.map aux args) | Cast (c,_,_) -> aux c - | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c) + | _ -> pattern_of_constr (Global.env())(*FIXME*) Evd.empty c in aux bodyi -- cgit v1.2.3