Merge branch 'master' of github.com:rlepigre/lambdapi

handle.ml

@@ -25,8 +25,8 @@ let handle_newdef : Sign.t -> string -> term -> unit = fun sign n a ->
   ignore (Typing.sort_type sign a); ignore (Sign.new_definable sign n a)
 
 (** [handle_defin sign x a t] extends [sign] with a definable symbol with name
-    [n] and type [a], and then adds a simple rewriting rule to  [t]. Note that
-    this amounts to defining a symbol with a single reduction rule. In case of
+    [x] and type [a], and then adds a simple rewriting rule to  [t]. Note that
+    this amounts to define a symbol with a single reduction rule. In case of
     error (typing, sorting, ...) the program fails gracefully. *)
 let handle_defin : Sign.t -> string -> term -> term -> unit = fun sg x a t ->
   ignore (Typing.sort_type sg a);
@@ -43,7 +43,7 @@ let handle_defin : Sign.t -> string -> term -> term -> unit = fun sg x a t ->
   in
   Sign.add_rule sg s rule
 
-(** [handle_rules sign rs] check that the rules of [rs] are well-typed, before
+(** [handle_rules sign rs] checks that the rules of [rs] are well-typed, before
     adding them to the corresponding symbol. The program fails gracefully when
     an error occurs. *)
 let handle_rules = fun sign rs ->