From a27ac0315dcbb99c64a260bac3988199a26b39cf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 15:14:19 +0100
Subject: Fix some documentation typos.

Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
---
 lib/profile.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/profile.ml b/lib/profile.ml
index 0910db3fe2..d620fe69c4 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
    number of allocated bytes may exceed the maximum integer capacity
    (2^31 on 32-bits architectures);  therefore, allocation is measured
    by small steps, total allocations are computed by adding elementary
-   measures and carries are controled from step to step *)
+   measures and carries are controlled from step to step *)
 
-(* Unix measure of time is approximative and shoitt delays are often
+(* Unix measure of time is approximate and short delays are often
    unperceivable; therefore, total times are measured in one (big)
    step to avoid rounding errors and to get the best possible
    approximation.
@@ -358,7 +358,7 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialisation, may be overriden *)
+(* Default initialization, may be overridden *)
 let _ = init_profile ()
 
 (******************************)
-- 
cgit v1.2.3


From 3e6fa1cbdc0ec145728089000595b6ea29f37a4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Nov 2016 16:35:56 +0100
Subject: Fix #5183 - Two CoqIDE crash errors

When opening a file without extension, an uncaught exception was
occurring.

Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
---
 lib/aux_file.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c6c7b42429..0f0f09aa23 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -17,6 +17,10 @@ let version = 1
 
 let oc = ref None
 
+let chop_extension f =
+  if check_suffix f ".v" then chop_extension f
+  else f
+
 let aux_file_name_for vfile =
   dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
 
-- 
cgit v1.2.3