diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 19:52:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:44 +0100 |
| commit | cbea91d815f134d63d02d8fb1bd78ed97db28cd1 (patch) | |
| tree | adeb71808e2f4d6be1686071e79e96cf6761f3c0 /plugins/cc/ccalgo.ml | |
| parent | 53fe23265daafd47e759e73e8f97361c7fdd331b (diff) | |
Tacmach API using EConstr.
Diffstat (limited to 'plugins/cc/ccalgo.ml')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc53b113d..102efe55b 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -508,7 +508,7 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_unsafe_type_of state.gls trm in + let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in let typ = canonize_name typ in let new_node= match t with @@ -832,7 +832,7 @@ let complete_one_class state i= let id = new_state_var etyp state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in let _c = pf_unsafe_type_of state.gls - (constr_of_term (term state.uf pac.cnode)) in + (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in |