diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-25 18:34:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:41 +0100 |
| commit | 02dd160233adc784eac732d97a88356d1f0eaf9b (patch) | |
| tree | d2baacdc2a4ae06e4607bfe09b48ba2c23a78a0f /plugins/cc/ccalgo.ml | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
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 |