From 505ac480574d235cd2f40ca4b2debde0bb875146 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 15 Sep 2016 17:32:22 +0200
Subject: typos

---
 interp/constrintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 30016dedcf..4502aa7ace 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -33,10 +33,10 @@ open Context.Rel.Declaration
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
-    - it remplaces notations by their value (scopes stuff are here)
+    - it replaces notations by their value (scopes stuff are here)
     - it recognizes global vars from local ones
-    - it prepares pattern maching problems (a pattern becomes a tree where nodes
-    are constructor/variable pairs and leafs are variables)
+    - it prepares pattern matching problems (a pattern becomes a tree
+      where nodes are constructor/variable pairs and leafs are variables)
 
     All that at once, fasten your seatbelt!
 *)
-- 
cgit v1.2.3