diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-01 23:47:59 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-01 23:47:59 +0100 |
| commit | d5b1807e65f7ea29d435c3f894aa551370c5989f (patch) | |
| tree | 48abae07dd6bb1087bc2cdd4a29d74a7419df350 /plugins/micromega/mfourier.ml | |
| parent | 53d109a21d97d073bc6a1f36a6c39b940a55eb69 (diff) | |
Fix typos.
Diffstat (limited to 'plugins/micromega/mfourier.ml')
| -rw-r--r-- | plugins/micromega/mfourier.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 0261d7349..e22fe5843 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 |