diff options
| author | Guillaume Melquiond | 2016-01-01 23:47:59 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-01 23:47:59 +0100 |
| commit | d5b1807e65f7ea29d435c3f894aa551370c5989f (patch) | |
| tree | 48abae07dd6bb1087bc2cdd4a29d74a7419df350 | |
| parent | 53d109a21d97d073bc6a1f36a6c39b940a55eb69 (diff) | |
Fix typos.
| -rw-r--r-- | ide/FAQ | 2 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 4 | ||||
| -rw-r--r-- | lib/hashcons.ml | 2 | ||||
| -rw-r--r-- | plugins/micromega/mfourier.ml | 4 |
4 files changed, 6 insertions, 6 deletions
@@ -1,7 +1,7 @@ CoqIde FAQ Q0) What is CoqIde? -R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations. +R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations. Q1) How to enable Emacs keybindings? R1: Insert diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 925b2248d8..6765f91ee1 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -277,7 +277,7 @@ exception CycleDetected problems. arXiv preprint arXiv:1112.0784. *) (* [delta] is the timeout for backward search. It might be - usefull to tune a multiplicative constant. *) + useful to tune a multiplicative constant. *) let get_delta g = int_of_float (min (float_of_int g.n_edges ** 0.5) @@ -668,7 +668,7 @@ let check_leq g u v = is_type0m_univ u || check_eq_univs g u v || real_check_leq g u v -(* enforc_univ_eq g u v will force u=v if possible, will fail otherwise *) +(* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *) let rec enforce_univ_eq u v g = let ucan = repr g u in diff --git a/lib/hashcons.ml b/lib/hashcons.ml index d927519181..eeaaf2f7fc 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -72,7 +72,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = end -(* A few usefull wrappers: +(* A few useful wrappers: * takes as argument the function [generate] above and build a function of type * u -> t -> t that creates a fresh table each time it is applied to the * sub-hcons functions. *) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 0261d73490..e22fe58434 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -120,7 +120,7 @@ and cstr_info = { (** A system of constraints has the form [\{sys = s ; vars = v\}]. [s] is a hashtable mapping a normalised vector to a [cstr_info] record where - [bound] is an interval - - [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint. + - [prf_idx] is the set of hypothesis indexes (i.e. constraints in the initial system) used to obtain the current constraint. In the initial system, each constraint is given an unique singleton proof_idx. When a new constraint c is computed by a function f(c1,...,cn), its proof_idx is ISet.fold union (List.map (fun x -> x.proof_idx) [c1;...;cn] - [pos] is the number of positive values of the vector @@ -872,7 +872,7 @@ let mk_proof hyps prf = | Elim(v,prf1,prf2) -> let prfsl = mk_proof prf1 and prfsr = mk_proof prf2 in - (* I take only the pairs for which the elimination is meaningfull *) + (* I take only the pairs for which the elimination is meaningful *) forall_pairs (pivot v) prfsl prfsr | And(prf1,prf2) -> let prfsl1 = mk_proof prf1 |