diff options
Diffstat (limited to 'plugins/cc/ccalgo.ml')
-rw-r--r-- | plugins/cc/ccalgo.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 0a980c03b..aedcb7575 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -452,8 +452,9 @@ and applist_projection c l = applistc (mkProj (p, hd)) tl) | _ -> applistc c l -let rec canonize_name c = - let func = canonize_name in +let rec canonize_name sigma c = + let c = EConstr.Unsafe.to_constr c in + let func c = canonize_name sigma (EConstr.of_constr c) in match kind_of_term c with | Const (kn,u) -> let canon_const = constant_of_kn (canonical_con kn) in @@ -509,7 +510,7 @@ let rec add_term state t= let b=next uf in let trm = constr_of_term t in let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in - let typ = canonize_name typ in + let typ = canonize_name (project state.gls) typ in let new_node= match t with Symb _ | Product (_,_) -> @@ -833,6 +834,7 @@ let complete_one_class state i= app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in let _c = pf_unsafe_type_of state.gls (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in + let _c = EConstr.Unsafe.to_constr _c in let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in |