From a05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 15 May 2017 03:00:04 +0200
Subject: Typo in comments of constrintern.

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3f99a3c7c..b57a04679 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -900,7 +900,7 @@ let interp_reference vars r =
 (**********************************************************************)
 (** {5 Cases }                                                        *)
 
-(** {6 Elemtary bricks } *)
+(** {6 Elementary bricks } *)
 let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
-- 
cgit v1.2.3