From 281bed69ee7d4a7638d07f07f9d6722b897f29cc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 3 Dec 2015 14:59:27 +0100 Subject: Improving over printing of let-tuple (see #4447). For instance, #4447 is now printed: λ Ca Da : ℕAlg, let (ℕ, ℕ0) := (Ca, Da) in let (C, p) := ℕ in let (c₀, cs) := p in let (D, p0) := ℕ0 in let (d₀, ds) := p0 in {h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type} : ℕAlg → ℕAlg → Type --- printing/ppconstr.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ea705e335e..663b8b8101 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -638,13 +638,13 @@ end) = struct | CLetTuple (_,nal,(na,po),c,b) -> return ( hv 0 ( - keyword "let" ++ spc () ++ - hov 0 (str "(" ++ + hov 2 (keyword "let" ++ spc () ++ + hov 1 (str "(" ++ prlist_with_sep sep_v pr_lname nal ++ str ")" ++ - pr_simple_return_type (pr mt) na po ++ str " :=" ++ - pr spc ltop c ++ spc () - ++ keyword "in") ++ + pr_simple_return_type (pr mt) na po ++ str " :=") ++ + pr spc ltop c + ++ keyword " in") ++ pr spc ltop b), lletin ) -- cgit v1.2.3 From f41968d8c240db4653d0b9fe76e1646cd7c6fb68 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 3 Dec 2015 19:08:51 +0100 Subject: Univs: fix bug #4443. Do not substitute rigid variables during minimization, keeping their equality constraints instead. --- library/universes.ml | 18 ++++++++++++------ test-suite/bugs/closed/4443.v | 31 +++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+), 6 deletions(-) create mode 100644 test-suite/bugs/closed/4443.v diff --git a/library/universes.ml b/library/universes.ml index a8e9478e13..3eae612c8c 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -205,7 +205,7 @@ let leq_constr_univs_infer univs m n = else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if Univ.check_leq univs u1 u2 then - ((if Univ.is_small_univ u1 then + ((if Univ.is_type0_univ u1 then cstrs := Constraints.add (u1, ULe, u2) !cstrs); true) else @@ -904,22 +904,28 @@ let normalize_context_set ctx us algs = let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in - let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> + let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> Constraint.add (canon, Univ.Eq, g) cst) global cstrs in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) rigid + cstrs + in let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in - (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) - (ctx, LMap.empty, Constraint.empty) partition + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, subst, us, cstrs)) + (ctx, LMap.empty, us, Constraint.empty) partition in (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = subst_univs_level_constraints subst noneqs in - let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in (* Compute the left and right set of flexible variables, constraints mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v new file mode 100644 index 0000000000..66dfa0e685 --- /dev/null +++ b/test-suite/bugs/closed/4443.v @@ -0,0 +1,31 @@ +Set Universe Polymorphism. + +Record TYPE@{i} := cType { + type : Type@{i}; +}. + +Definition PROD@{i j k} + (A : Type@{i}) + (B : A -> Type@{j}) + : TYPE@{k}. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + +Local Unset Strict Universe Declaration. +Definition PRODinj + (A : Type@{i}) + (B : A -> Type) + : TYPE. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + + Monomorphic Universe i j. + Monomorphic Constraint j < i. +Set Printing Universes. +Check PROD@{i i i}. +Check PRODinj@{i j}. +Fail Check PRODinj@{j i}. \ No newline at end of file -- cgit v1.2.3 From 9ee4a02e9234ad6cebb3365881250d7539d00d03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 4 Dec 2015 15:14:23 +0100 Subject: Fix in setoid_rewrite in Type: avoid the generation of a rigid universe on applications of inverse (flip) on a crelation. This was poluting universe constraints of lemmas using generalized rewriting in Type. --- tactics/rewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 182c232ae9..a230ea251a 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -403,7 +403,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in + let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end -- cgit v1.2.3 From cbceffe424a6b4477eb822f3887776b587503cbd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 00:42:24 +0100 Subject: Fix CHANGES. --- CHANGES | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/CHANGES b/CHANGES index 662b7b9a24..96f02bc27c 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,10 @@ +Changes from V8.5beta3 +====================== + +Specification language + +- Syntax "$(tactic)$" changed to "ltac:(tactic)". + Changes from V8.5beta2 to V8.5beta3 =================================== @@ -10,10 +17,6 @@ Vernacular commands introducing it. - New command "Show id" to show goal named id. -Specification language - -- Syntax "$(tactic)$" changed to "ltac: tactic". - Tactics - New flag "Regular Subst Tactic" which fixes "subst" in situations where -- cgit v1.2.3 From 387351b4c0ffeff65d8a7192f5073cfd4bd20f53 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 00:14:37 +0100 Subject: Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. --- CHANGES | 5 +++++ doc/refman/RefMan-tac.tex | 47 ++++++++++++++++++------------------------- parsing/g_tactic.ml4 | 17 +++++++++++++++- test-suite/success/destruct.v | 2 +- 4 files changed, 42 insertions(+), 29 deletions(-) diff --git a/CHANGES b/CHANGES index 96f02bc27c..70ed1bef01 100644 --- a/CHANGES +++ b/CHANGES @@ -5,6 +5,11 @@ Specification language - Syntax "$(tactic)$" changed to "ltac:(tactic)". +Tactics + +- Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly + for induction. + Changes from V8.5beta2 to V8.5beta3 =================================== diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 03c4f6a365..55b5f622ff 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1531,25 +1531,27 @@ for each possible form of {\term}, i.e. one for each constructor of the inductive or co-inductive type. Unlike {\tt induction}, no induction hypothesis is generated by {\tt destruct}. -If the argument is dependent in either the conclusion or some -hypotheses of the goal, the argument is replaced by the appropriate -constructor form in each of the resulting subgoals, thus performing -case analysis. If non-dependent, the tactic simply exposes the -inductive or co-inductive structure of the argument. - There are special cases: \begin{itemize} \item If {\term} is an identifier {\ident} denoting a quantified -variable of the conclusion of the goal, then {\tt destruct {\ident}} -behaves as {\tt intros until {\ident}; destruct {\ident}}. + variable of the conclusion of the goal, then {\tt destruct {\ident}} + behaves as {\tt intros until {\ident}; destruct {\ident}}. If + {\ident} is not anymore dependent in the goal after application of + {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as {\tt intros until {\num}} followed by {\tt destruct} applied to the last introduced hypothesis. Remark: For destruction of a numeral, use syntax {\tt destruct ({\num})} (not very interesting anyway). +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). + \item The argument {\term} can also be a pattern of which holes are denoted by ``\_''. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are @@ -1626,14 +1628,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway). They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using}, and {\tt in} clauses. -\item{\tt destruct !{\ident}} - - This is a case when the destructed term is an hypothesis of the - context. The ``!'' modifier tells to keep the hypothesis in the - context after destruction. - - This applies also to the other form of {\tt destruct} and {\tt edestruct}. - \item{\tt case \term}\label{case}\tacindex{case} The tactic {\tt case} is a more basic tactic to perform case @@ -1699,14 +1693,22 @@ There are particular cases: \begin{itemize} \item If {\term} is an identifier {\ident} denoting a quantified -variable of the conclusion of the goal, then {\tt induction {\ident}} -behaves as {\tt intros until {\ident}; induction {\ident}}. + variable of the conclusion of the goal, then {\tt induction + {\ident}} behaves as {\tt intros until {\ident}; induction + {\ident}}. If {\ident} is not anymore dependent in the goal + after application of {\tt induction}, it is erased (to avoid + erasure, use parentheses, as in {\tt induction ({\ident})}). \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as {\tt intros until {\num}} followed by {\tt induction} applied to the last introduced hypothesis. Remark: For simple induction on a numeral, use syntax {\tt induction ({\num})} (not very interesting anyway). +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt induction}, it is erased (to avoid erasure, use + parentheses, as in {\tt induction ({\ident})}). + \item The argument {\term} can also be a pattern of which holes are denoted by ``\_''. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are @@ -1821,15 +1823,6 @@ Show 2. einduction}. It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:}, {\tt using}, and {\tt in} clauses. -\item{\tt induction !{\ident}} - - This is a case when the term on which to apply induction is an - hypothesis of the context. The ``!'' modifier tells to keep the - hypothesis in the context after induction. - - This applies also to the other form of {\tt induction} and {\tt - einduction}. - \item {\tt elim \term}\label{elim} This is a more basic induction tactic. Again, the type of the diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b7559a1989..4d42dfe85a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -44,6 +44,20 @@ let test_lpar_id_coloneq = | _ -> err ()) | _ -> err ()) +(* Hack to recognize "(x)" *) +let test_lpar_id_rpar = + Gram.Entry.of_parser "lpar_id_coloneq" + (fun strm -> + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ")" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" @@ -224,8 +238,9 @@ GEXTEND Gram ; induction_arg: [ [ n = natural -> (None,ElimOnAnonHyp n) + | test_lpar_id_rpar; c = constr_with_bindings -> + (Some false,induction_arg_of_constr c) | c = constr_with_bindings -> (None,induction_arg_of_constr c) - | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c) ] ] ; constr_with_bindings_arg: diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 59cd25cd76..9f091e3996 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -389,7 +389,7 @@ Abort. Goal forall b:bool, True. intro b. -destruct !b. +destruct (b). clear b. (* b has to be here *) Abort. -- cgit v1.2.3 From 1dfb2c020fa0ed2e853539b8b398a9d91cbbeefa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Oct 2015 23:28:16 +0200 Subject: RefMan, ch. 4: Minor changes for spacing, clarity. --- doc/refman/RefMan-cic.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 3fd5ae0b24..15b8fb9c8d 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -109,7 +109,7 @@ sets, namely the sorts {\Set} and {\Type$(j)$} for $jProp) : Type %a recursive argument and $(x:_P T)C$ if the argument is not recursive. \paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}} +\label{Sort-polymorphism-inductive} From {\Coq} version 8.1, inductive families declared in {\Type} are polymorphic over their arguments in {\Type}. If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity obtained from $A$ by replacing its sort with $s$. Especially, if $A$ -is well-typed in some environment and context, then $A_{/s}$ is typable +is well-typed in some global environment and local context, then $A_{/s}$ is typable by typability of all products in the Calculus of Inductive Constructions. The following typing rule is added to the theory. \begin{description} \item[Ind-Family] Let $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ be an inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$ - be its context of parameters, $\Gamma_I = [I_1:\forall + be its local context of parameters, $\Gamma_I = [I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of definitions and $\Gamma_C = [c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of @@ -1105,7 +1108,7 @@ a strongly normalizing reduction, we cannot accept any sort of recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals. -For instance, assuming a parameter $A:\Set$ exists in the context, we +For instance, assuming a parameter $A:\Set$ exists in the local context, we want to build a function \length\ of type $\ListA\ra \nat$ which computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$ and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$. We want these @@ -1364,7 +1367,7 @@ constructor have type \Prop. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort $s$ is legal. Typical examples are the conjunction of non-informative propositions and the equality. -If there is an hypothesis $h:a=b$ in the context, it can be used for +If there is an hypothesis $h:a=b$ in the local context, it can be used for rewriting not only in logical propositions but also in any type. % In that case, the term \verb!eq_rec! which was defined as an axiom, is % now a term of the calculus. @@ -1438,8 +1441,8 @@ only constructors of $I$. \paragraph{Example.} For \List\ and \Length\ the typing rules for the {\tt match} expression -are (writing just $t:M$ instead of \WTEG{t}{M}, the environment and -context being the same in all the judgments). +are (writing just $t:M$ instead of \WTEG{t}{M}, the global environment and +local context being the same in all the judgments). \[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~ f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))} -- cgit v1.2.3 From fe2776f9e0d355cccb0841495a9843351d340066 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Oct 2015 08:14:39 +0200 Subject: RefMan, ch. 1 and 2: avoiding using the name "constant" when "constructor" and "inductive" are meant also. --- doc/refman/RefMan-ext.tex | 10 +++++----- doc/refman/RefMan-gal.tex | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 80e12898f0..a2be25c3ba 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1250,7 +1250,7 @@ possible, the correct argument will be automatically generated. \end{ErrMsgs} -\subsection{Declaration of implicit arguments for a constant +\subsection{Declaration of implicit arguments \comindex{Arguments}} \label{ImplicitArguments} @@ -1263,7 +1263,7 @@ a priori and a posteriori. \subsubsection{Implicit Argument Binders} In the first setting, one wants to explicitly give the implicit -arguments of a constant as part of its definition. To do this, one has +arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly braces: \begin{coq_eval} Reset Initial. @@ -1300,7 +1300,7 @@ usual implicit arguments disambiguation syntax. \subsubsection{Declaring Implicit Arguments} -To set implicit arguments for a constant a posteriori, one can use the +To set implicit arguments a posteriori, one can use the command: \begin{quote} \tt Arguments {\qualid} \nelist{\possiblybracketedident}{} @@ -1379,7 +1379,7 @@ Check (fun l => map length l = map (list nat) nat length l). \Rem To know which are the implicit arguments of an object, use the command {\tt Print Implicit} (see \ref{PrintImplicit}). -\subsection{Automatic declaration of implicit arguments for a constant} +\subsection{Automatic declaration of implicit arguments} {\Coq} can also automatically detect what are the implicit arguments of a defined object. The command is just @@ -1582,7 +1582,7 @@ Implicit arguments names can be redefined using the following syntax: \end{quote} Without the {\tt rename} flag, {\tt Arguments} can be used to assert -that a given constant has the expected number of arguments and that +that a given object has the expected number of arguments and that these arguments are named as expected. \noindent {\bf Example (continued): } diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 9b527053c3..e49c82d8fd 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -971,7 +971,7 @@ are the names of its constructors and {\type$_1$}, {\ldots}, {\type$_n$} their respective types. The types of the constructors have to satisfy a {\em positivity condition} (see Section~\ref{Positivity}) for {\ident}. This condition ensures the soundness of the inductive -definition. If this is the case, the constants {\ident}, +definition. If this is the case, the names {\ident}, {\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with their respective types. Accordingly to the universe where the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a @@ -990,7 +990,7 @@ Inductive nat : Set := \end{coq_example} The type {\tt nat} is defined as the least \verb:Set: containing {\tt - O} and closed by the {\tt S} constructor. The constants {\tt nat}, + O} and closed by the {\tt S} constructor. The names {\tt nat}, {\tt O} and {\tt S} are added to the environment. Now let us have a look at the elimination principles. They are three @@ -1101,7 +1101,7 @@ Inductive list (A:Set) : Set := \end{coq_example*} Note that in the type of {\tt nil} and {\tt cons}, we write {\tt - (list A)} and not just {\tt list}.\\ The constants {\tt nil} and + (list A)} and not just {\tt list}.\\ The constructors {\tt nil} and {\tt cons} will have respectively types: \begin{coq_example} -- cgit v1.2.3 From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 7 Dec 2015 10:52:14 +0100 Subject: Fix some typos. --- dev/v8-syntax/syntax-v8.tex | 2 +- doc/refman/Program.tex | 4 ++-- doc/refman/RefMan-tac.tex | 8 ++++---- kernel/closure.ml | 2 +- kernel/fast_typeops.ml | 6 +++--- kernel/opaqueproof.mli | 4 ++-- plugins/extraction/extraction.ml | 4 ++-- plugins/funind/functional_principles_proofs.mli | 2 +- plugins/funind/recdef.ml | 12 ++++++------ plugins/romega/refl_omega.ml | 8 ++++---- plugins/setoid_ring/InitialRing.v | 6 +++--- plugins/setoid_ring/Ncring_initial.v | 4 ++-- tactics/tactics.ml | 6 +++--- test-suite/Makefile | 2 +- theories/FSets/FMapFacts.v | 2 +- theories/FSets/FMapPositive.v | 2 +- theories/MMaps/MMapFacts.v | 2 +- theories/MMaps/MMapPositive.v | 2 +- theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +- theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +- theories/Numbers/NatInt/NZDiv.v | 2 +- theories/Numbers/Natural/Abstract/NDiv.v | 2 +- theories/Numbers/Natural/Abstract/NParity.v | 2 +- theories/Program/Subset.v | 2 +- theories/Structures/EqualitiesFacts.v | 2 +- theories/Structures/OrderedType.v | 2 +- theories/Structures/OrdersLists.v | 2 +- theories/ZArith/Zdiv.v | 2 +- theories/ZArith/Zpow_alt.v | 2 +- theories/ZArith/Zquot.v | 2 +- 31 files changed, 52 insertions(+), 52 deletions(-) diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 6630be06ab..64431ea161 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -81,7 +81,7 @@ Parenthesis are used to group regexps. Beware to distinguish this operator $\GR{~}$ from the terminals $\ETERM{( )}$, and $\mid$ from terminal \TERMbar. -Rules are optionaly annotated in the right margin with: +Rules are optionally annotated in the right margin with: \begin{itemize} \item a precedence and associativity (L for left, R for right and N for no associativity), indicating how to solve conflicts; lower levels are tighter; diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 8e078e9814..3a99bfdd4f 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -201,7 +201,7 @@ in their context. In this case, the obligations should be transparent recursive calls can be checked by the kernel's type-checker. There is an optimization in the generation of obligations which gets rid of the hypothesis corresponding to the -functionnal when it is not necessary, so that the obligation can be +functional when it is not necessary, so that the obligation can be declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the context, the proof of the obligation is \emph{required} to be declared transparent. @@ -216,7 +216,7 @@ properties. It will generate obligations, try to solve them automatically and fail if some unsolved obligations remain. In this case, one can first define the lemma's statement using {\tt Program Definition} and use it as the goal afterwards. -Otherwise the proof will be started with the elobarted version as a goal. +Otherwise the proof will be started with the elaborated version as a goal. The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt Hypothesis}, {\tt Axiom} etc... diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 55b5f622ff..f367f04c43 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3555,7 +3555,7 @@ The hints for \texttt{auto} and \texttt{eauto} are stored in databases. Each database maps head symbols to a list of hints. One can use the command \texttt{Print Hint \ident} to display the hints associated to the head symbol \ident{} (see \ref{PrintHint}). Each -hint has a cost that is an nonnegative integer, and an optional pattern. +hint has a cost that is a nonnegative integer, and an optional pattern. The hints with lower cost are tried first. A hint is tried by \texttt{auto} when the conclusion of the current goal matches its pattern or when it has no pattern. @@ -3772,7 +3772,7 @@ Hint Extern 4 (~(_ = _)) => discriminate. with hints with a cost less than 4. One can even use some sub-patterns of the pattern in the tactic - script. A sub-pattern is a question mark followed by an ident, like + script. A sub-pattern is a question mark followed by an identifier, like \texttt{?X1} or \texttt{?X2}. Here is an example: % Require EqDecide. @@ -3815,7 +3815,7 @@ The \texttt{emp} regexp does not match any search path while \texttt{eps} matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a list of identifiers for the hints (note \texttt{Hint Extern}'s do not have an -associated identitier). Before applying any hint $\ident$ the current +associated identifier). Before applying any hint $\ident$ the current path $p$ extended with $\ident$ is matched against the current cut expression $c$ associated to the hint database. If matching succeeds, the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$ @@ -4672,7 +4672,7 @@ Use \texttt{classical\_right} to prove the right part of the disjunction with th %% procedure for first-order intuitionistic logic implemented in {\em %% NuPRL}\cite{Kre02}. -%% Search may optionnaly be bounded by a multiplicity parameter +%% Search may optionally be bounded by a multiplicity parameter %% indicating how many (at most) copies of a formula may be used in %% the proof process, its absence may lead to non-termination of the tactic. diff --git a/kernel/closure.ml b/kernel/closure.ml index ea9b2755f2..03e70495fb 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -771,7 +771,7 @@ let drop_parameters depth n argstk = (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 063c9cf126..b625478f25 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -33,7 +33,7 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) +(* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = match kind_of_term(whd_betadeltaiota env t) with | Sort s -> {utj_val = c; utj_type = s } @@ -52,8 +52,8 @@ let assumption_of_judgment env t ty = error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 0609c8517e..009ff82ff5 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -11,9 +11,9 @@ open Term open Mod_subst (** This module implements the handling of opaque proof terms. - Opauqe proof terms are special since: + Opaque proof terms are special since: - they can be lazily computed and substituted - - they are stoked in an optionally loaded segment of .vo files + - they are stored in an optionally loaded segment of .vo files An [opaque] proof terms holds the real data until fully discharged. In this case it is called [direct]. When it is [turn_indirect] the data is relocated to an opaque table diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6ae519ef60..1112c3b890 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -734,7 +734,7 @@ and extract_cst_app env mle mlt kn u args = if la >= ls then (* Enough args, cleanup already done in [mla], we only add the - additionnal dummy if needed. *) + additional dummy if needed. *) put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla)) else (* Partially applied function with some logical arg missing. @@ -748,7 +748,7 @@ and extract_cst_app env mle mlt kn u args = (*s Extraction of an inductive constructor applied to arguments. *) (* \begin{itemize} - \item In ML, contructor arguments are uncurryfied. + \item In ML, constructor arguments are uncurryfied. \item We managed to suppress logical parts inside inductive definitions, but they must appears outside (for partial applications for instance) \item We also suppressed all Coq parameters to the inductives, since diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 61fce267a3..34ce669672 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -8,7 +8,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : - constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *) + constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) constr option ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5d41ec7237..951bef2beb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -203,7 +203,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob -(* Debuging mechanism *) +(* Debugging mechanism *) let debug_queue = Stack.create () let rec print_debug_queue b e = @@ -291,9 +291,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = -(* Travelling term. +(* Traveling term. Both definitions of [f_terminate] and [f_equation] use the same generic - travelling mechanism. + traveling mechanism. *) (* [check_not_nested forbidden e] checks that [e] does not contains any variable @@ -327,7 +327,7 @@ let check_not_nested forbidden e = with UserError(_,p) -> errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) -(* ['a info] contains the local information for travelling *) +(* ['a info] contains the local information for traveling *) type 'a infos = { nb_arg : int; (* function number of arguments *) concl_tac : tactic; (* final tactic to finish proofs *) @@ -337,7 +337,7 @@ type 'a infos = f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) - func : global_reference; (* functionnal reference *) + func : global_reference; (* functional reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) @@ -357,7 +357,7 @@ type ('a,'b) journey_info_tac = 'b infos -> (* argument of the tactic *) tactic -(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term +(* journey_info : specifies the actions to do on the different term constructors during the traveling of the term *) type journey_info = { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac; diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 95407c5ff1..560e6a899e 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -46,7 +46,7 @@ let occ_step_eq s1 s2 = match s1, s2 with d'une liste de pas à partir de la racine de l'hypothèse *) type occurrence = {o_hyp : Names.Id.t; o_path : occ_path} -(* \subsection{refiable formulas} *) +(* \subsection{reifiable formulas} *) type oformula = (* integer *) | Oint of Bigint.bigint @@ -55,7 +55,7 @@ type oformula = | Omult of oformula * oformula | Ominus of oformula * oformula | Oopp of oformula - (* an atome in the environment *) + (* an atom in the environment *) | Oatom of int (* weird expression that cannot be translated *) | Oufo of oformula @@ -75,7 +75,7 @@ type oproposition = | Pimp of int * oproposition * oproposition | Pprop of Term.constr -(* Les équations ou proposiitions atomiques utiles du calcul *) +(* Les équations ou propositions atomiques utiles du calcul *) and oequation = { e_comp: comparaison; (* comparaison *) e_left: oformula; (* formule brute gauche *) @@ -1266,7 +1266,7 @@ let resolution env full_reified_goal systems_list = | (O_right :: l) -> app coq_p_right [| loop l |] in let correct_index = let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in - (* PL: it seems that additionnally introduced hyps are in the way during + (* PL: it seems that additionally introduced hyps are in the way during normalization, hence this index shifting... *) if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce) in diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index b92b847be5..56023bfb5c 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -155,7 +155,7 @@ Section ZMORPHISM. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. -(*morphisms are extensionaly equal*) +(*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;simpl; try rewrite (same_gen ARth);rrefl. @@ -246,7 +246,7 @@ Proof (SRth_ARth Nsth Nth). Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y. Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed. -(**Same as above : definition of two,extensionaly equal, generic morphisms *) +(**Same as above : definition of two, extensionally equal, generic morphisms *) (**from N to any semi-ring*) Section NMORPHISM. Variable R : Type. @@ -671,7 +671,7 @@ End GEN_DIV. end. (* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above - are only optimisations that directly returns the reifid constant + are only optimisations that directly returns the reified constant instead of resorting to the constant propagation of the simplification algorithm. *) Ltac inv_gen_phi rO rI cO cI t := diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index c40e0ffbaa..c2eafcdad8 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -42,7 +42,7 @@ Defined. (*Instance ZEquality: @Equality Z:= (@eq Z).*) -(** Two generic morphisms from Z to (abrbitrary) rings, *) +(** Two generic morphisms from Z to (arbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. Context {R:Type}`{Ring R}. @@ -130,7 +130,7 @@ Ltac rsimpl := simpl. Qed. -(*morphisms are extensionaly equal*) +(*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. destruct x;rsimpl; try rewrite same_gen; reflexivity. diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3e6cea5ddd..ce8b9b3dbd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3205,7 +3205,7 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = mkProd (Anonymous, eq, lift 1 concl), [| refl |] else concl, [||] in - (* Abstract by equalitites *) + (* Abstract by equalities *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in (* Abstract by the "generalized" hypothesis. *) @@ -3216,11 +3216,11 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in - (* Then apply to the original instanciated hyp. *) + (* Then apply to the original instantiated hyp. *) let instc = Option.cata (fun _ -> instc) (mkApp (instc, [| mkVar id |])) body in (* Apply the reflexivity proofs on the indices. *) let appeqs = mkApp (instc, Array.of_list refls) in - (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) + (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) mkApp (appeqs, abshypt) let hyps_of_vars env sign nogen hyps = diff --git a/test-suite/Makefile b/test-suite/Makefile index 7150d1fd4f..207f25ed0b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v fi; \ } > "$@" -# Additionnal dependencies for module tests +# Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v $(HIDE)$(coqtop) -R modules Mods -compile $< diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 8c6f4b64a7..eaeb2914b3 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -2143,7 +2143,7 @@ Module OrdProperties (M:S). Section Fold_properties. (** The following lemma has already been proved on Weak Maps, - but with one additionnal hypothesis (some [transpose] fact). *) + but with one additional hypothesis (some [transpose] fact). *) Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 3eac15b038..9e59f0c505 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -1061,7 +1061,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End PositiveMap. -(** Here come some additionnal facts about this implementation. +(** Here come some additional facts about this implementation. Most are facts that cannot be derivable from the general interface. *) diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v index 69066a7b6d..8b356d7501 100644 --- a/theories/MMaps/MMapFacts.v +++ b/theories/MMaps/MMapFacts.v @@ -2381,7 +2381,7 @@ Module OrdProperties (M:S). Section Fold_properties. (** The following lemma has already been proved on Weak Maps, - but with one additionnal hypothesis (some [transpose] fact). *) + but with one additional hypothesis (some [transpose] fact). *) Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v index d3aab2389d..adbec70574 100644 --- a/theories/MMaps/MMapPositive.v +++ b/theories/MMaps/MMapPositive.v @@ -641,7 +641,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End PositiveMap. -(** Here come some additionnal facts about this implementation. +(** Here come some additional facts about this implementation. Most are facts that cannot be derivable from the general interface. *) Module PositiveMapAdditionalFacts. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d0df8fb4a7..ab73ebfe1d 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -391,7 +391,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0 a < b*q -> a/b < q. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index d5f3f4ada7..c8260e516f 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -436,7 +436,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0 a < b*q -> a/b < q. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index de2e99ec3a..464fe354b8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -404,7 +404,7 @@ Proof. intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto. Qed. -(** Some additionnal inequalities about quot. *) +(** Some additional inequalities about quot. *) Theorem quot_lt_upper_bound: forall a b q, 0<=a -> 0 a < b*q -> a÷b < q. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 4a127216f8..e0dfdedbd5 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -307,7 +307,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0<=a -> 0 a < b*q -> a/b < q. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index fb68c139b5..d3d3eb0fbb 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -137,7 +137,7 @@ Proof. intros; apply mul_succ_div_gt; auto'. Qed. Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). Proof. intros. apply div_exact; auto'. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, b~=0 -> a < b*q -> a/b < q. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index b3526c9a17..80a579f19f 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -8,7 +8,7 @@ Require Import Bool NSub NZParity. -(** Some additionnal properties of [even], [odd]. *) +(** Some additional properties of [even], [odd]. *) Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 50b89b5c07..ce1f7768dd 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -82,7 +82,7 @@ Qed. Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B := fn (exist _ x eq_refl). -(* This is what we want to be able to do: replace the originaly matched object by a new, +(* This is what we want to be able to do: replace the originally matched object by a new, propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *) Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 8e2b2d081c..d5827d87a0 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType). Hint Resolve eqke_1 eqke_2 eqk_1. - (* Additionnal facts *) + (* Additional facts *) Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) : InA eqke p m -> InA eqk p m. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index cc8c2261b6..93ca383b28 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -342,7 +342,7 @@ Module KeyOrderedType(O:OrderedType). compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto. Qed. - (* Additionnal facts *) + (* Additional facts *) Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 4d49ac84ed..41e65d7287 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -76,7 +76,7 @@ Module KeyOrderedType(O:OrderedType). Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt). Proof. eapply subrelation_proper; eauto with *. Qed. - (* Additionnal facts *) + (* Additional facts *) Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt). Proof. apply pair_compat. Qed. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index d0d10891a2..363b4fd03e 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -279,7 +279,7 @@ Proof. intros; rewrite Z.div_exact; auto. Qed. Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a. Proof. intros. apply Z.mod_le; auto. Qed. -(** Some additionnal inequalities about Z.div. *) +(** Some additional inequalities about Z.div. *) Theorem Zdiv_lt_upper_bound: forall a b q, 0 < b -> a < q*b -> a/b < q. diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v index 8f661a9c80..c8627477be 100644 --- a/theories/ZArith/Zpow_alt.v +++ b/theories/ZArith/Zpow_alt.v @@ -11,7 +11,7 @@ Local Open Scope Z_scope. (** An alternative power function for Z *) -(** This [Zpower_alt] is extensionnaly equal to [Z.pow], +(** This [Zpower_alt] is extensionally equal to [Z.pow], but not convertible with it. The number of multiplications is logarithmic instead of linear, but these multiplications are bigger. Experimentally, it seems diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 3ef1118986..6db92edb70 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -243,7 +243,7 @@ Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. -(** Some additionnal inequalities about Zdiv. *) +(** Some additional inequalities about Zdiv. *) Theorem Zquot_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a÷b <= q. -- cgit v1.2.3 From 19ea51a4b7f7debbe5bdeb2b2689cddadd9876f4 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 7 Dec 2015 16:25:58 +0100 Subject: Fixing a minor problem in Makefile.build that was prevening "dev/printers.cma" to be loadable within "ocamldebug". --- Makefile.build | 6 +++--- dev/db | 2 -- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Makefile.build b/Makefile.build index 98ef81f38c..00ff6a7a4c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -133,9 +133,9 @@ SYSCMA:=$(addsuffix .cma,$(SYSMOD)) SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) ifeq ($(CAMLP4),camlp5) -P4CMA:=gramlib.cma +P4CMA:=gramlib.cma str.cma else -P4CMA:=dynlink.cma camlp4lib.cma +P4CMA:=dynlink.cma camlp4lib.cma str.cma endif @@ -882,7 +882,7 @@ dev/printers.cma: | dev/printers.mllib.d $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $^ -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -linkall -a -o $@ grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' diff --git a/dev/db b/dev/db index f259b50eb3..36a171af1c 100644 --- a/dev/db +++ b/dev/db @@ -1,5 +1,3 @@ -load_printer "gramlib.cma" -load_printer "str.cma" load_printer "printers.cma" install_printer Top_printers.ppfuture -- cgit v1.2.3