aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-24 16:59:15 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-27 18:49:46 +0200
commit18dca1c4310b66e012bea9a47c481676190baa5e (patch)
tree92a96e8a160c58559c1b09075a0eecdb44712fd1 /plugins/cc
parent46a7ac14e5803d1690584ac939889ecc03ab0dd4 (diff)
Congruence: typography in a comment.
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5cab6d203..39348a3e7 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -9,7 +9,7 @@
(************************************************************************)
(* This file implements the basic congruence-closure algorithm by *)
-(* Downey,Sethi and Tarjan. *)
+(* Downey, Sethi and Tarjan. *)
(* Plus some e-matching and constructor handling by P. Corbineau *)
open CErrors