From 1c228b648cb1755cad3ec1f38690110d6fe14bc5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 5 May 2019 16:58:10 +0200
Subject: rewrite.ml: remove outdated comment

---
 plugins/ltac/rewrite.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 950115146b..6f84e6c18d 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1977,7 +1977,6 @@ let warn_add_morphism_deprecated =
 let add_morphism_infer ~pstate atts m n : Proof_global.t option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
-  (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
-- 
cgit v1.2.3