diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index c8238804a0..473199cb2a 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -400,9 +400,12 @@ let rec canonize_name c = (* rebuild a term from a pattern and a substitution *) let build_subst uf subst = - Array.map (fun i -> - try term uf i - with _ -> anomaly (Pp.str "incomplete matching")) subst + Array.map + (fun i -> + try term uf i + with e when Errors.noncritical e -> + anomaly (Pp.str "incomplete matching")) + subst let rec inst_pattern subst = function PVar i -> |