From fe99efdbe409e47f20776c62a76d4de7f0188afc Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 11 Apr 2017 12:46:23 +0200
Subject: Update various comments to use "template polymorphism"

Also remove obvious comments.
---
 engine/universes.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/universes.mli b/engine/universes.mli
index 932de941a6..83ca1ea606 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -223,7 +223,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s
 
 val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
 
-(** {6 Support for old-style sort-polymorphism } *)
+(** {6 Support for template polymorphism } *)
 
 val solve_constraints_system : universe option array -> universe array -> universe array ->
   universe array
-- 
cgit v1.2.3