diff options
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | doc/refman/Polynom.tex | 15 | ||||
| -rw-r--r-- | kernel/inductive.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 8 |
4 files changed, 17 insertions, 16 deletions
diff --git a/Makefile.common b/Makefile.common index fead1dac6..7c98b64de 100644 --- a/Makefile.common +++ b/Makefile.common @@ -78,12 +78,12 @@ SRCDIRS:=\ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils -# Order is relevent here because kernel and checker contain files +# Order is relevant here because kernel and checker contain files # with the same name CHKSRCDIRS:= checker lib config kernel parsing ########################################################################### -# tools +# Tools ########################################################################### COQDEP:=bin/coqdep$(EXE) diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index a2c09b824..974a56247 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -288,7 +288,7 @@ the following property: The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$ -($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used +($mod_1$,\dots,$mod_2$)}. The name is not relevant. It is just used for error messages. The term $ring$ is a proof that the ring signature satisfies the (semi-)ring axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list @@ -314,7 +314,7 @@ describes their syntax and effects: \item[constants [\ltac]] specifies a tactic expression that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns {\tt - InitialRing.NotConstant}. The default behaviour is to map only 0 and + InitialRing.NotConstant}. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. \item[preprocess [\ltac]] @@ -470,7 +470,8 @@ correctness theorem to well-chosen arguments. The {\tt field} tactic is an extension of the {\tt ring} to deal with -rational expresision. Given a rational expression $F=0$. It first reduces the expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring +rational expression. Given a rational expression $F=0$. It first reduces the +expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring expressions. For example, if we take $F = (1 - 1/x) x - x + 1$, this gives $ N= (x -1) x - x^2 + x$ and $D= x$. It then calls {\tt ring} @@ -539,7 +540,7 @@ Reset Initial. $D_2$. This way, polynomials remain in factorized form during the fraction simplifications. This yields smaller expressions when reducing to the same denominator since common factors can be - cancelled. + canceled. \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$]} performs the simplification in the conclusion of the goal using @@ -627,11 +628,11 @@ denominator during the normalization process. These expressions must be proven different from zero for the correctness of the algorithm. The syntax for adding a new field is {\tt Add Field $name$ : $field$ -($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used +($mod_1$,\dots,$mod_2$)}. The name is not relevant. It is just used for error messages. $field$ is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is -used to tailor the behaviour of the tactic. Since field tactics are -built upon ring tactics, all mofifiers of the {\tt Add Ring} +used to tailor the behavior of the tactic. Since field tactics are +built upon ring tactics, all modifiers of the {\tt Add Ring} apply. There is only one specific modifier: \begin{description} \item[completeness \term] allows the field tactic to prove diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a08184ed5..577367aa0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -394,7 +394,7 @@ let type_case_branches env (pind,largs) pj c = (************************************************************************) -(* Checking the case annotation is relevent *) +(* Checking the case annotation is relevant *) let check_case_info env (indsp,u) ci = let (mib,mip as spec) = lookup_mind_specif env indsp in @@ -637,7 +637,7 @@ let abstract_mind_lc ntyps npars lc = (* [get_recargs_approx env tree ind args] builds an approximation of the recargs tree for ind, knowing args. The argument tree is used to know when candidate nested types should be traversed, pruning the tree otherwise. This code is very -close to check_positive in indtypes.ml, but does no positivy check and does not +close to check_positive in indtypes.ml, but does no positivity check and does not compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = @@ -662,7 +662,7 @@ let get_recargs_approx env tree ind args = mk_norec and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) = - (* If the infered tree already disallows recursion, no need to go further *) + (* If the inferred tree already disallows recursion, no need to go further *) if eq_wf_paths tree mk_norec then tree else let mib = Environ.lookup_mind mind env in diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 05bf3dc98..bde263d21 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -20,7 +20,7 @@ type input_buffer = { mutable prompt : unit -> string; mutable str : string; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) - mutable bols : int list; (* offsets in str of begining of lines *) + mutable bols : int list; (* offsets in str of beginning of lines *) mutable tokens : Gram.parsable; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) @@ -31,7 +31,7 @@ let resize_buffer ibuf = String.blit ibuf.str 0 nstr 0 (String.length ibuf.str); ibuf.str <- nstr -(* Delete all irrelevent lines of the input buffer. Keep the last line +(* Delete all irrelevant lines of the input buffer. Keep the last line in the buffer (useful when there are several commands on the same line. *) let resynch_buffer ibuf = @@ -280,7 +280,7 @@ let parse_to_dot = in Gram.Entry.of_parser "Coqtoplevel.dot" dot -(* If an error occured while parsing, we try to read the input until a dot +(* If an error occurred while parsing, we try to read the input until a dot token is encountered. We assume that when a lexer error occurs, at least one char was eaten *) @@ -306,7 +306,7 @@ let read_sentence () = - End_of_input: Ctrl-D was typed in, we will quit. In particular, this is normally the only place where a Sys.Break - is catched and handled (i.e. not re-raised). + is caught and handled (i.e. not re-raised). *) let do_vernac () = |