aboutsummaryrefslogtreecommitdiff
path: root/contrib/first-order
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/first-order')
-rw-r--r--contrib/first-order/ground.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 418e6ce831..00a2260c6f 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -45,17 +45,17 @@ let update_flags ()=
*)
let update_flags ()=
- let predref=ref Names.KNpred.empty in
+ let predref=ref Names.Cpred.empty in
let f coe=
try
let kn=destConst (Classops.get_coercion_value coe) in
- predref:=Names.KNpred.add kn !predref
+ predref:=Names.Cpred.add kn !predref
with Invalid_argument "destConst"-> () in
List.iter f (Classops.coercions ());
red_flags:=
Closure.RedFlags.red_add_transparent
Closure.betaiotazeta
- (Names.Idpred.full,Names.KNpred.complement !predref)
+ (Names.Idpred.full,Names.Cpred.complement !predref)
let ground_tac solver startseq gl=
update_flags ();