From d306f5428db0d034aea55d3f0699c67c1f296cc1 Mon Sep 17 00:00:00 2001
From: JPR
Date: Thu, 23 May 2019 23:28:55 +0200
Subject: Fixing typos - Part 3

---
 printing/ppconstr.ml    | 2 +-
 printing/proof_diffs.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 9d3ed40f6c..e495b1af41 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -348,7 +348,7 @@ let tag_var = tag Tag.variable
             hov 1 (str "`" ++ (surround_impl b'
                                  (pr_lident CAst.(make ?loc id) ++ str " : " ++
                                     (if t' then str "!" else mt()) ++ pr t)))
-          |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
+          |_ -> anomaly (Pp.str "List of generalized binders have always one element.")
         end
       | Default b ->
         match t with
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index f378a5d2dd..abb0d55b39 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -408,7 +408,7 @@ the call to db_goal_map and entering the following:
 let match_goals ot nt =
   let nevar_to_oevar = ref StringMap.empty in
   (* ogname is "" when there is no difference on the current path.
-     It's set to the old goal's evar name once a rewitten goal is found,
+     It's set to the old goal's evar name once a rewritten goal is found,
      at which point the code only searches for the replacing goals
      (and ot is set to nt). *)
   let iter2 f l1 l2 =
-- 
cgit v1.2.3