diff options
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2expr.mli | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2intern.mli | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2match.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index 1069d0bfa3..2e7dfc42db 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -173,7 +173,7 @@ type strexpr = (** {5 Dynamic semantics} *) -(** Values are represented in a way similar to OCaml, i.e. they constrast +(** Values are represented in a way similar to OCaml, i.e. they contrast immediate integers (integers, constructors without arguments) and structured blocks (tuples, arrays, constructors with arguments), as well as a few other base cases, namely closures, strings, named constructors, and dynamic type diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli index d646b5cda5..829570a354 100644 --- a/user-contrib/Ltac2/tac2intern.mli +++ b/user-contrib/Ltac2/tac2intern.mli @@ -20,7 +20,7 @@ val is_value : glb_tacexpr -> bool val check_unit : ?loc:Loc.t -> type_scheme -> unit val check_subtype : type_scheme -> type_scheme -> bool -(** [check_subtype t1 t2] returns [true] iff all values of intances of type [t1] +(** [check_subtype t1 t2] returns [true] iff all values of instances of type [t1] also have type [t2]. *) val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml index 058d02adde..354a578cb3 100644 --- a/user-contrib/Ltac2/tac2match.ml +++ b/user-contrib/Ltac2/tac2match.ml @@ -88,7 +88,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) |