diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index aba908d482..fbe31fe527 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -427,7 +427,8 @@ let rec add_term state t= try Termhash.find uf.syms t with Not_found -> let b=next uf in - let typ = pf_type_of state.gls (constr_of_term t) in + let trm = Termops.refresh_universes (constr_of_term t) in + let typ = pf_type_of state.gls trm in let typ = canonize_name typ in let new_node= match t with |