diff options
| -rw-r--r-- | pretyping/constr_matching.ml | 1 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index afdf601c21..daac33f503 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -84,7 +84,6 @@ let rec build_lambda vars ctx m = match vars with | n :: vars -> (* change [ x1 ... xn y z1 ... zm |- t ] into [ x1 ... xn z1 ... zm |- lam y. t ] *) - let len = List.length ctx in let pre, suf = List.chop (pred n) ctx in let (na, t, suf) = match suf with | [] -> assert false diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 349c05a38d..0787b058ae 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -520,7 +520,7 @@ let warn_skip_spaces_curly = (fun () ->strbrk "Skipping spaces inside curly brackets") let rec drop_spacing = function - | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt + | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt | fmt -> fmt |