aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-02-02 10:18:48 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 12:17:34 +0100
commitd91a0c27402f0f19a30147bb9d87387ca2a91fd0 (patch)
treeb0ea13cb3186f8a405b3980c11571b19cc81f7aa /ide
parent2189505b6e50c9a9aa8e9d520c05461e59f18d04 (diff)
"Standardizing" the name LocalPatten into LocalRawPattern.
Diffstat (limited to 'ide')
-rw-r--r--ide/texmacspp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 6fbed38fb..7bbf393ac 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -235,7 +235,7 @@ and pp_local_binder lb = (* don't know what it is for now *)
let ppl =
List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
xmlTyped (ppl @ [pp_expr ce])
- | LocalPattern _ ->
+ | LocalRawPattern _ ->
assert false
and pp_local_decl_expr lde = (* don't know what it is for now *)
match lde with