From 3e0bf68bdc1ac6bde7bd04236657fb4d554817ad Mon Sep 17 00:00:00 2001
From: mcaci
Date: Sat, 12 Oct 2019 14:24:18 +0200
Subject: Doc update with mlg extension - fix #10855

---
 plugins/cc/README     | 2 +-
 plugins/cc/ccproof.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/README b/plugins/cc/README
index c616b5daab..7df7b971e8 100644
--- a/plugins/cc/README
+++ b/plugins/cc/README
@@ -9,7 +9,7 @@ Files :
 
 - ccalgo.ml : congruence closure algorithm
 - ccproof.ml : proof generation code
-- cctac.ml4 : the tactic itself
+- cctac.mlg : the tactic itself
 - CCSolve.v : a small Ltac tactic based on congruence 
 
 Known Bugs : the congruence tactic can fail due to type dependencies.
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index ef012e5092..f47a14cdc7 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (* This file uses the (non-compressed) union-find structure to generate *)
-(* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
+(* proof-trees that will be transformed into proof-terms in cctac.mlg   *)
 
 open CErrors
 open Constr
-- 
cgit v1.2.3