diff --git a/Engine/Prefix.v b/Engine/Prefix.v
index 8f007c1..1573e13 100644
--- a/Engine/Prefix.v
+++ b/Engine/Prefix.v
@@ -621,7 +621,7 @@ Proof.
     repeat rewrite Character.numeric_pseudo_bij in H4.
     assumption.
   } subst.
-  repeat rewrite (canonicalize_casesenst rer _ no_i_flag) in H2.
+  repeat rewrite (Character.canonicalize_casesenst rer _ no_i_flag) in H2.
   symmetry. apply EqDec.inversion_true. assumption.
 Qed.
 
@@ -778,7 +778,7 @@ Proof.
   intros rest s c cd no_i_flag Hstart Hmatch.
 
   Ltac unfold_match H no_i_flag :=
-    unfold char_match in H; rewrite (canonicalize_casesenst _ _ no_i_flag) in H.
+    unfold char_match in H; rewrite (Character.canonicalize_casesenst _ _ no_i_flag) in H.
 
   induction cd;
     (* there is no known literal *)
@@ -786,7 +786,7 @@ Proof.
   (* CdSingle *)
   - unfold_match Hmatch no_i_flag.
     assert (c = c0). {
-      simpl in Hmatch. rewrite (canonicalize_casesenst _ _ no_i_flag) in Hmatch.
+      simpl in Hmatch. rewrite (Character.canonicalize_casesenst _ _ no_i_flag) in Hmatch.
       eqdec. reflexivity.
     } subst.
     simpl.
@@ -802,12 +802,12 @@ Proof.
     + etransitivity.
       * eapply starts_with_chain_merge_literals.
         intro. eapply extract_literal_char_impossible_no_match; eauto.
-      * eapply IHcd1. unfold char_match. rewrite canonicalize_casesenst; eauto.
+      * eapply IHcd1. unfold char_match. rewrite Character.canonicalize_casesenst; eauto.
     + simpl. rewrite merge_literals_comm.
       etransitivity.
       * eapply starts_with_chain_merge_literals.
         intro. eapply extract_literal_char_impossible_no_match; eauto.
-      * eapply IHcd2. unfold char_match. rewrite canonicalize_casesenst; eauto.
+      * eapply IHcd2. unfold char_match. rewrite Character.canonicalize_casesenst; eauto.
 Qed.
 
 (* generalization of extract_literal_prefix on the group map and the list of actions *)
diff --git a/Rewriting/Anchors.v b/Rewriting/Anchors.v
index f90f7a6..68ede2d 100644
--- a/Rewriting/Anchors.v
+++ b/Rewriting/Anchors.v
@@ -151,6 +151,6 @@ Section Anchors.
     Anchor a ≅[rer] desugar_anchor a.
   Proof.
     intros Hic; apply desugar_anchor_correct.
-    all: intros c; try rewrite canonicalize_casesenst; intuition.
+    all: intros c; try rewrite Character.canonicalize_casesenst; intuition.
   Qed.
 End Anchors.
diff --git a/Semantics/Chars.v b/Semantics/Chars.v
index dfeaf78..ebf2e4f 100644
--- a/Semantics/Chars.v
+++ b/Semantics/Chars.v
@@ -82,7 +82,7 @@ Section Chars.
   Proof.
     intro Hcasesenst.
     induction l; simpl; auto.
-    rewrite canonicalize_casesenst, IHl by auto. auto.
+    rewrite Character.canonicalize_casesenst, IHl by auto. auto.
   Qed.
 
   Lemma inb_canonicalized_casesenst:
@@ -90,7 +90,7 @@ Section Chars.
     forall c l, inb_canonicalized c l = inb c l.
   Proof.
     intros Hcasesenst c l. unfold inb_canonicalized.
-    rewrite canonicalize_casesenst by assumption.
+    rewrite Character.canonicalize_casesenst by assumption.
     rewrite map_canonicalize_casesenst by assumption.
     reflexivity.
   Qed.
diff --git a/Semantics/Inst.v b/Semantics/Inst.v
index efabb0c..61938ab 100644
--- a/Semantics/Inst.v
+++ b/Semantics/Inst.v
@@ -7,12 +7,5 @@ using a naive instantiation of Warblre typeclasses *)
 
 Instance character_class: Character.class := @Parameters.character_class parameters.
 
-Lemma canonicalize_casesenst: forall rer chr, RegExpRecord.ignoreCase rer = false -> Character.canonicalize rer chr = chr.
-Proof.
-  intros rer chr Hcasesenst.
-  unfold Character.canonicalize, character_class, Parameters.character_class, parameters, NaiveEngineParameters.Character.canonicalize.
-  rewrite Hcasesenst. reflexivity.
-Qed.
-
 Instance naive_params: LindenParameters :=
-  lindenParameters_of_warblre parameters canonicalize_casesenst.
+  lindenParameters_of_warblre parameters.
diff --git a/Semantics/Parameters.v b/Semantics/Parameters.v
index 9f9f862..9196ec3 100644
--- a/Semantics/Parameters.v
+++ b/Semantics/Parameters.v
@@ -8,21 +8,15 @@ Class LindenParameters := make {
   #[global] char:: Character.class; (* a type of characters, *)
   #[global] unicodeProp:: Parameters.Property.class (@Parameters.Character char); (* a type of Unicode properties, *)
   #[global] charset_class:: @CharSet.class char; (* and a type of character sets. *)
-
-  (* As per the ECMA specification (22.2.2.7.3 Canonicalize ( rer, ch )), when we do not ignore case, canonicalization is the identity function. *)
-  canonicalize_casesenst: forall rer chr, RegExpRecord.ignoreCase rer = false -> Character.canonicalize rer chr = chr;
 }.
 
 Section OfWarblre.
   Context (p: Parameters).
-  Context (canon: forall rer chr,
-              RegExpRecord.ignoreCase rer = false ->
-              Character.canonicalize rer chr = chr).
 
   Definition lindenParameters_of_warblre : LindenParameters :=
     make
       (@Parameters.character_class p)
       (@Parameters.unicode_property_class p)
-      (@Parameters.set_class p)
-      canon.
+      (@Parameters.set_class p).
+
 End OfWarblre.
diff --git a/linden.opam b/linden.opam
index 54f1d6b..11f9231 100644
--- a/linden.opam
+++ b/linden.opam
@@ -30,5 +30,5 @@ build: [
 ]
 x-maintenance-intent: ["(latest)"]
 pin-depends: [
-  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#cb2dab9d197a22e4284497200682793b97bf4121"]
+  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#4321379b887d590a42759818f6d9b1fd2351688e"]
 ]
diff --git a/linden.opam.template b/linden.opam.template
index b2bc0a2..36c0945 100644
--- a/linden.opam.template
+++ b/linden.opam.template
@@ -1,3 +1,3 @@
 pin-depends: [
-  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#cb2dab9d197a22e4284497200682793b97bf4121"]
+  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#4321379b887d590a42759818f6d9b1fd2351688e"]
 ]