aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-01-11 16:57:34 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-01-11 16:57:34 +0000
commitbe4fe5a4351ad7b315983c5959daf8ff6c7a193e (patch)
tree74c0f2fdc8a15b8fa1234d8bd23bc6be0606c69b /library
parent6668aecbd325d77e6d04e09931eefcabbe8342bf (diff)
Fix some typos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/libobject.ml4
-rw-r--r--library/libobject.mli6
2 files changed, 5 insertions, 5 deletions
diff --git a/library/libobject.ml b/library/libobject.ml
index 4cc2fdb35..bc62913d9 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -16,7 +16,7 @@ open Mod_subst
wants to work with restricted Coq programs that have only parts of
the full capabilities, but may still be able to work correctly for
limited purposes. One example is for the graphical interface, that uses
- such a limite coq process to do only parsing. It loads .vo files, but
+ such a limited Coq process to do only parsing. It loads .vo files, but
is only interested in loading the grammar rule definitions. *)
let relax_flag = ref false;;
@@ -55,7 +55,7 @@ let default_object s = {
declare_object { (default_object "MY OBJECT") with
cache_function = fun (sp,a) -> Mytbl.add sp a}
- and the listed functions are only those which definitions accually
+ and the listed functions are only those which definitions actually
differ from the default.
This helps introducing new functions in objects.
diff --git a/library/libobject.mli b/library/libobject.mli
index ad4468fb8..57c3debe9 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -15,12 +15,12 @@ open Mod_subst
* a caching function specifying how to add the object in the current
scope;
If the object wishes to register its visibility in the Nametab,
- it should do so for all possible sufixes.
+ it should do so for all possible suffixes.
* a loading function, specifying what to do when the module
containing the object is loaded;
If the object wishes to register its visibility in the Nametab,
- it should do so for all sufixes no shorter than the "int" argument
+ it should do so for all suffixes no shorter than the "int" argument
* an opening function, specifying what to do when the module
containing the object is opened (imported);
@@ -35,7 +35,7 @@ open Mod_subst
the module name must be updated
Keep - the object is not substitutive, but survives module
closing
- Anticipate - this is for objects that have to be explicitely
+ Anticipate - this is for objects that have to be explicitly
managed by the [end_module] function (like Require
and Read markers)