diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index d84a9d2eda..701c8f7079 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -120,7 +120,7 @@ type tomatch_stack = tomatch_status list originating from a subterm in which case real args are not dependent; it accounts for n+1 binders if dep or n binders if not dep - [PrProd] types abstracted term ([Abstract]); it accounts for one binder - - [PrCcl] types the right-hand-side + - [PrCcl] types the right-hand side - Aliases [Alias] have no trace in [predicate_signature] *) @@ -1147,7 +1147,7 @@ let rec generalize_problem pb = function tomatch = Abstract d :: tomatch; pred = Option.map (generalize_predicate i d) pb'.pred } -(* No more patterns: typing the right-hand-side of equations *) +(* No more patterns: typing the right-hand side of equations *) let build_leaf pb = let rhs = extract_rhs pb in let tycon = match pb.pred with @@ -1924,7 +1924,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra let typing_fun tycon env = typing_fun tycon env isevars in - (* We build the matrix of patterns and right-hand-side *) + (* We build the matrix of patterns and right-hand side *) let matx = matx_of_eqns env eqns in (* We build the vector of terms to match consistently with the *) |