From df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 23 Feb 2015 11:26:51 +0100 Subject: Fix some typos in comments. --- proofs/proofview.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/proofview.ml') diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a25683bfc..b6861fd49 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -192,8 +192,8 @@ let unfocus c sp = succeed). Another benefit is that it is possible to write tactics that can be executed even if there are no focused goals. - Tactics form a monad ['a tactic], in a sense a tactic can be - seens as a function (without argument) which returns a value of - type 'a and modifies the environement (in our case: the view). + seen as a function (without argument) which returns a value of + type 'a and modifies the environment (in our case: the view). Tactics of course have arguments, but these are given at the meta-level as OCaml functions. Most tactics in the sense we are used to return [()], that is no really interesting values. But @@ -1126,7 +1126,7 @@ module V82 = struct (* Returns the open goals of the proofview together with the evar_map to - interprete them. *) + interpret them. *) let goals { comb = comb ; solution = solution; } = { Evd.it = comb ; sigma = solution } -- cgit v1.2.3