diff --git a/CHANGES.md b/CHANGES.md
index b4d727f2e..6d17acae4 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -23,6 +23,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Export to Lean.
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
 - Extend `print` query to the following arguments: `verbose`, `debug`, `flag`, `builtin`, `prover`, `prover_timeout`.
+- Conditional rules `l when t1 ≡ t2 ↪ r`
 
 ### Changed
 
diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index 17e18f47a..9e1c2a57c 100644
--- a/doc/lambdapi.bnf
+++ b/doc/lambdapi.bnf
@@ -35,6 +35,10 @@
 <constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
+         | <term> when <condition> "↪" <term>
+
+<condition> ::= <term> ≡ <term>
+              | <term> «[<term>] <term>
 
 <unif_rule> ::= <equation> "↪" "[" <equation> (";" <equation>)* "]"
 
diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el
index 2b9ad2b30..c004074a2 100644
--- a/editors/emacs/lambdapi-smie.el
+++ b/editors/emacs/lambdapi-smie.el
@@ -56,7 +56,8 @@
      "rule"
      "symbol"
      "unif_rule"
-     "verbose")
+     "verbose"
+     "when")
    lambdapi--queries)
   "Commands at top level.")
 
@@ -142,7 +143,9 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
       (symdec ("symbol" args ":" sterm))
       (indcons (args ":" sterm) ("|" args ":" sterm))
       (inddec (inddec "with" args ":" sterm "≔" indcons))
-      (rules (rules "with" sterm "↪" sterm))
+      (rules (rules "with" sterm "↪" sterm)
+             (rules "with" sterm "when" condition "↪" sterm))
+      (condition (sterm "«[" sterm "]" sterm) (sterm "≡" sterm))
       (command
                ("begin" prfcontent "abort" ";")
                ("begin" prfcontent "admitted" ";")
@@ -240,7 +243,7 @@ The default lexer is used because the syntax is primarily made of sexps."
                       "print" "proofterm" "search" "type"))
      (lambdapi--query-indent))
 
-    (`(,_ . ,(or "," "↪" "→" "≡")) (smie-rule-separator kind))
+    (`(,_ . ,(or "«" "," "↪" "→" "≡")) (smie-rule-separator kind))
 
     (`(,(or :before :list-intro) . ,(or "≔" ":")) (smie-rule-separator kind))
     (`(:after . ,(or "≔" ":")) lambdapi-indent-basic)
diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el
index d5f54afdb..57513f00c 100644
--- a/editors/emacs/lambdapi-vars.el
+++ b/editors/emacs/lambdapi-vars.el
@@ -47,6 +47,7 @@
     "rule"
     "symbol"
     "unif_rule"
+    "when"
     "with")
   "Commands that enrich the signature.")
 
@@ -106,6 +107,7 @@
     (modify-syntax-entry ?→ "." table)
     (modify-syntax-entry ?↪ "." table)
     (modify-syntax-entry ?≔ "." table)
+    (modify-syntax-entry ?« "." table)
     (modify-syntax-entry ?$ "." table)
     (modify-syntax-entry ?? "." table)
     (modify-syntax-entry ?: "." table)
diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim
index 4e485eb42..5c1635815 100644
--- a/editors/vim/syntax/lambdapi.vim
+++ b/editors/vim/syntax/lambdapi.vim
@@ -98,6 +98,7 @@ syntax keyword KeywordOK contained type
 syntax keyword KeywordOK contained TYPE
 syntax keyword KeywordOK contained unif_rule
 syntax keyword KeywordOK contained verbose
+syntax keyword KeywordOK contained when
 syntax keyword KeywordOK contained why3
 syntax keyword KeywordOK contained with
 highlight link KeywordOK Keyword
@@ -172,6 +173,7 @@ syntax keyword KeywordKO contained type
 syntax keyword KeywordKO contained TYPE
 syntax keyword KeywordKO contained unif_rule
 syntax keyword KeywordKO contained verbose
+syntax keyword KeywordKO contained when
 syntax keyword KeywordKO contained why3
 syntax keyword KeywordKO contained with
 highlight link KeywordKO Error
@@ -207,6 +209,7 @@ syntax match Keyword ","
 syntax match Keyword ";"
 syntax match Keyword "_"
 syntax match Keyword "≡"
+syntax match Keyword "«"
 
 " Other special classes.
 syntax match Type "\u\w*"
@@ -215,6 +218,7 @@ syntax match PreProc  "?\(\<\h\w*\>\|\({|\([^|]\|\(|[^}]\)\)*|*|}\)\)"
 
 " Abbreviations.
 abbreviate --> ↪
+abbreviate << «
 abbreviate -> →
 abbreviate => ⇒
 abbreviate !  Π
diff --git a/editors/vscode/syntaxes/lp.tmLanguage.json b/editors/vscode/syntaxes/lp.tmLanguage.json
index e7a25f740..bbf5d44ff 100644
--- a/editors/vscode/syntaxes/lp.tmLanguage.json
+++ b/editors/vscode/syntaxes/lp.tmLanguage.json
@@ -45,7 +45,7 @@
     },
 
     "signature-commands": {
-      "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with)\\s+([^\\s+]*)",
+      "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with|when)\\s+([^\\s+]*)",
       "captures": {
         "1": {"name": "storage.type.lp"},
         "2": {"name": "entity.name.function.theorem.lp"}
diff --git a/misc/lambdapi.tex b/misc/lambdapi.tex
index 02d29e67b..7b4f739ad 100644
--- a/misc/lambdapi.tex
+++ b/misc/lambdapi.tex
@@ -9,7 +9,7 @@
   tabsize=2,
   basicstyle={\ttfamily\small\upshape},
   backgroundcolor=\color{lightgrey},
-  keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with},
+  keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with,when},
   sensitive=true,
   keywordstyle=\color{blue},
   morecomment=[l]{//},
@@ -26,6 +26,7 @@
   {≔}{$\coloneqq$}1
   {⊢}{$\vdash$}1
   {≡}{$\equiv$}1
+  {«}{$\ll$}1
   {𝔹}{$\mathbb{B}$}1
   {𝕃}{$\mathbb{L}$}1
   {ℕ}{$\mathbb{N}$}1
diff --git a/src/core/coercion.ml b/src/core/coercion.ml
index 3faf8bb5b..7cc708ecc 100644
--- a/src/core/coercion.ml
+++ b/src/core/coercion.ml
@@ -15,6 +15,6 @@ let _ =
     and t = mk_Patt (Some 1, "t", [||]) in
     let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in
     { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0;
-      rule_pos = None }
+      rule_pos = None; r_when = R_None }
   in
   Sign.add_rule Ghost.sign (coerce, rule)
diff --git a/src/core/eval.ml b/src/core/eval.ml
index 99463434f..d4f85373e 100644
--- a/src/core/eval.ml
+++ b/src/core/eval.ml
@@ -291,6 +291,33 @@ and tree_walk : config -> sym -> stack -> (term * stack) option =
   let (lazy capacity, lazy tree) = cfg.dtree s in
   let vars = Array.make capacity mk_Kind in (* dummy terms *)
   let bound = Array.make capacity None in
+  (* [ct2t t] transforms a contraint to a term by replacing pattern variables
+     by their values *)
+  let rec ct2t : Tree_type.c_term -> term = fun t ->
+    match t with
+    | Tree_type.C_App ((p,s), al) ->
+        add_args (mk_Symb (Sign.find_qualified p s)) (List.map ct2t al)
+    | C_Patt pv -> vars.(fst pv)
+    | C_Sym (p,s) -> mk_Symb (Sign.find_qualified p s)
+  in
+  (* [flatten op t] returns the list of arguments of [op]
+     considered as associative at the top level of [t] *)
+  let flatten: sym -> term -> term list = fun sy t ->
+    let rec flatten acc t =
+      match get_args t with
+      | (Symb s, al) when s == sy -> List.fold_left flatten acc al
+      | _ -> t::acc
+    in flatten [] t
+  in
+  (* [rebuild op u l] applies the binary [op] on arguments of [l],
+     returns [u] if [l] is empty.
+   *)
+  let rebuild: sym -> term -> term list -> term = fun sy u l ->
+    match l with
+    | [] -> u
+    | [t] -> t
+    | _ -> List.fold_left (fun a t -> mk_Appl(a,t)) (mk_Symb sy) l
+  in
   (* [walk tree stk cursor vars_id id_vars] where [stk] is the stack of terms
      to match and [cursor] the cursor indicating where to write in the [vars]
      array described in {!module:Term} as the environment of the RHS during
@@ -342,6 +369,59 @@ and tree_walk : config -> sym -> stack -> (term * stack) option =
               let vi = Array.map (fun id -> mk_Vari (var id)) vi in
               let tj = msubst bj vi in
               if eq_modulo whnf cfg vars.(i) tj then ok else fail
+          | CondEQ(((p1,o1) as op1,a1), ((p2,o2) as op2,a2)) ->
+              let v1 = List.map (fun (i,_) -> vars.(i)) a1 in
+              let v2 = List.map (fun (i,_) -> vars.(i)) a2 in
+              if Logger.log_enabled() then
+                log_rew "%aCondEQ(%s[%a],%s[%a]) : %s(%a) == %s(%a)"
+                  D.depth !depth
+                  (snd op1) (List.pp D.int ",") (List.map fst a1)
+                  (snd op2) (List.pp D.int ",") (List.map fst a2)
+                  (snd op1) (List.pp Raw.term ",") v1
+                  (snd op2) (List.pp Raw.term ",") v2;
+              let s1 = Sign.find_qualified p1 o1 in
+              let s2 = Sign.find_qualified p2 o2 in
+              let t1 = add_args (mk_Symb s1) v1 in
+              let t2 = add_args (mk_Symb s2) v2 in
+              if eq_modulo whnf cfg t1 t2 then ok else fail
+
+          (* find_doubles ty! op! n! t! d? before? middle? after? *)
+          | CondCHK((_,"#find_doubles"), [ty;C_App((p,o),[]);u;t;d;b;m;a]) ->
+              if Logger.log_enabled() then
+                log_rew "%aCondCHK(\"find_doubles\",%s,%a,%a) : %a %a"
+                  D.depth !depth
+                  o c_term u c_term t Raw.term (ct2t u) Raw.term (ct2t t);
+              let sy = Sign.find_qualified p o in
+              let _ty = ct2t ty and u = ct2t u and t = ct2t t in
+              let d,b,m,a = ct2t d, ct2t b, ct2t m, ct2t a in
+              let rec doubles l =
+                match l with
+                  [] -> raise Not_found
+                | t::l' ->
+                    try
+                      let (b,_,a) = List.split (fun u -> Term.cmp t u = 0) l'
+                      in (t, [], b, a)
+                    with Not_found ->
+                      let (d,b,m,a) = doubles l' in
+                      (d,(t::b),m,a)
+              in
+              begin
+                try
+                  let t = snf (whnf cfg) t in
+                  let (sd,sb,sm,sa) = doubles (flatten sy t) in
+                  let sb = rebuild sy u sb in
+                  let sm = rebuild sy u sm in
+                  let sa = rebuild sy u sa in
+                  if eq_modulo whnf cfg sd d
+                     && eq_modulo whnf cfg sb b
+                     && eq_modulo whnf cfg sm m
+                     && eq_modulo whnf cfg sa a then
+                    ok
+                  else
+                    fail
+                with Not_found -> fail
+              end
+          | CondCHK((_pth,_op), _args) -> fail
           | CondFV(i,xs) ->
               let allowed =
                 (* Variables that are allowed in the term. *)
diff --git a/src/core/libMeta.ml b/src/core/libMeta.ml
index bff70f3e1..60d7720b0 100644
--- a/src/core/libMeta.ml
+++ b/src/core/libMeta.ml
@@ -37,7 +37,14 @@ let set : problem -> meta -> mbinder -> unit = fun p m v ->
 let make : problem -> ctxt -> term -> term = fun p ctx a ->
   let a,k = Ctxt.to_prod ctx a in
   let m = fresh p a k in
-  mk_Meta(m, Array.of_list (List.rev_map (fun (x,_,_) -> mk_Vari x) ctx))
+(*
+  mk_Meta(m, Array.of_list (List.rev_map (fun (x,_,_) -> mk_Vari x) ctx)) 
+*)
+  mk_Meta(m, Array.of_list (List.filter_rev_map 
+                              (fun (x,_,v) -> if v=None then
+                                                Some (mk_Vari x) else None)
+                              ctx))  
+ (* jpb *) 
 
 (** [make_codomain p ctx a] creates a fresh metavariable term of type [Type]
     in the context [ctx] extended with a fresh variable of type [a], and
diff --git a/src/core/sign.ml b/src/core/sign.ml
index 329cd423a..31e3694bc 100644
--- a/src/core/sign.ml
+++ b/src/core/sign.ml
@@ -137,14 +137,15 @@ let link : t -> unit = fun sign ->
   and link_term = link_term mk_Appl in
   let link_rule r =
     let lhs = List.map link_lhs r.lhs in
+    let arity = List.length lhs in
     let rhs = link_term r.rhs in
-    {r with lhs ; rhs}
+    {r with lhs ; rhs; arity}  (* jpb *)
   in
   let f _ s =
     s.sym_type := link_term !(s.sym_type);
     s.sym_def := Option.map link_term !(s.sym_def);
     s.sym_rules := List.map link_rule !(s.sym_rules);
-    Tree.update_dtree s []
+    Tree.update_dtree s [];
   in
   StrMap.iter f !(sign.sign_symbols);
   let f mp {dep_symbols=sm; _} =
diff --git a/src/core/term.ml b/src/core/term.ml
index 68601a386..918524677 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -211,6 +211,20 @@ and sym =
 
 (** {3 Representation of rewriting rules} *)
 
+(** terms in rule constraints *)
+and r_term =
+  | R_App of sym * r_term list  (* application *)
+  | R_Patt of int               (* pattern variable *)
+  | R_Sym of sym                (* global symbol *)
+
+(** optional rule constraints *)
+and r_constraint =
+  (* equality constraint f p1 ... pn == g q1 ... qm *)
+  | R_EQ of (sym * int list) * (sym * int list)
+  (* predefined constraint *)
+  | R_CHK of sym * r_term list
+  | R_None (* no constraint *)
+
 (** Representation of a rewriting rule. A rewriting rule is mainly formed of a
     LHS (left hand side),  which is the pattern that should be matched for the
     rule to apply, and a RHS (right hand side) giving the action to perform if
@@ -219,6 +233,7 @@ and sym =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
+  ; r_when   : r_constraint (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
@@ -993,3 +1008,35 @@ module Raw = struct
   let term = term let _ = term
   let ctxt = ctxt let _ = ctxt
 end
+
+(** {4 functions over constraints} *)
+
+(** [rAll p t] checks [p] on all pattern variables of [t] *)
+let rec rAll : (int -> bool) -> r_term -> bool = fun p t ->
+  match t with
+  | R_App(_s,al) -> List.for_all (rAll p) al
+  | R_Patt i -> p i
+  | R_Sym _ -> true
+
+(** [rFind f t] applies [f] to each pvar of [t] and returns the first 
+    successful result, None if all calls fail. *)
+let rec rFind : (int -> 'a option) -> r_term -> 'a option = fun f t ->
+  match t with
+  | R_App(_s,al) -> List.find_map (rFind f) al
+  | R_Patt i -> f i
+  | R_Sym _ -> None
+
+(** [rFold o a t] computes [a o pv1 o ... pvn] where pv1...pvn are the 
+    pattern variables of t. *)
+let rec rFold : ('a -> int -> 'a) -> 'a -> r_term -> 'a = fun f a t ->
+  match t with
+  | R_App(_s,al) -> List.fold_left (rFold f) a al
+  | R_Patt i -> f a i
+  | R_Sym _ -> a
+
+(** Printing function for debug *)
+let rec r_term : r_term pp = fun ppf t ->
+  match t with
+  | R_App (s,al) -> out ppf "(%a %a)" sym s (List.pp r_term " ") al
+  | R_Patt i -> out ppf "?%d" i
+  | R_Sym s -> out ppf "%a" sym s
diff --git a/src/core/term.mli b/src/core/term.mli
index 701b18774..670eb2b16 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -140,6 +140,20 @@ and sym =
 
 (** {3 Representation of rewriting rules} *)
 
+(** terms in rule constraints *)
+and r_term =
+  | R_App of sym * r_term list  (* application *)
+  | R_Patt of int               (* pattern variable *)
+  | R_Sym of sym                (* global symbol *)
+
+(** optional rule constraints *)
+and r_constraint =
+  (* equality constraint f p1 ... pn == g q1 ... qm *)
+  | R_EQ of (sym * int list) * (sym * int list)
+  (* predefined constraint *)
+  | R_CHK of sym * r_term list
+  | R_None (* no constraint *)
+
 (** Representation of a rewriting rule. A rewriting rule is mainly formed of a
     LHS (left hand side),  which is the pattern that should be matched for the
     rule to apply, and a RHS (right hand side) giving the action to perform if
@@ -148,6 +162,7 @@ and rule =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
+  ; r_when   : r_constraint (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
@@ -177,8 +192,8 @@ and rule =
        concrete syntax) are represented in the same way, and with a unique
        name (in the rule) that is generated automatically.
 
-    Then, the term [f t u v w] matches the LHS with a substitution represented
-    by an array of terms [a] of length 3 if we
+    Then, the term [f t u v w] matches the LHS with a substitution
+    represented by an array of terms [a] of length 3 if we
     have [a.(0) = t], [a.(1) = u], [a.(1) = v] and [a.(2) = w].
 
     {b TODO} memorising [w] in the substitution is sub-optimal. In practice,
@@ -468,3 +483,20 @@ module Raw : sig
   val term : term pp
   val ctxt : ctxt pp
 end
+
+(** {4 functions over constraints} *)
+
+(** [rAll p t] checks [p] on all pattern variables of [t]. *)
+val rAll : (int -> bool) -> r_term -> bool
+
+(** [rFind f t] applies [f] to each pvar of [t] and returns the first
+    successful result, None if all calls fail. *)
+val rFind : (int -> 'a option) -> r_term -> 'a option
+
+(** [rFold o a t] computes [a o pv1 o ... pvn] where pv1...pvn are the 
+    pattern variables of t. *)
+val rFold : ('a -> int -> 'a) -> 'a -> r_term -> 'a
+
+(** Printing function for debug *)
+val r_term : r_term pp
+
diff --git a/src/core/tree.ml b/src/core/tree.ml
index dfbe2190e..9959d827e 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -71,6 +71,20 @@ module CP = struct
       let compare = Stdlib.compare
     end)
 
+  (** Functional sets of pairs of flat terms. *)
+  module TSet = Set.Make(
+    struct
+      type t = (psym * pvar list) * (psym * pvar list)
+      let compare = Stdlib.compare
+    end)
+
+  (** Functional sets of predefined constraints. *)
+  module CHKSet = Set.Make(
+    struct
+      type t = psym * c_term list
+      let compare = Stdlib.compare
+    end)
+
   (** A pool of (convertibility and free variable) conditions. *)
   type t =
     { variables : pvar IntMap.t
@@ -85,17 +99,27 @@ module CP = struct
     ; fv_conds : int array IntMap.t
     (** A mapping of [i] to [xs] represents a free variable condition that can
         only be satisfied if only the free variables of [x] appear in the term
-        stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) }
+        stored at slot [i] in the [vars] array of [Eval.tree_walk]. *)
+    ; eq_conds : TSet.t
+    (** Set of pairs of terms that should be convertible. *)
+    ; chk_conds : CHKSet.t
+    (** sets of predefined constraints. *)
+    }
 
   (** [empty] is the condition pool holding no condition. *)
   let empty : t =
     { variables = IntMap.empty
     ; nl_conds = PSet.empty
-    ; fv_conds = IntMap.empty }
+    ; fv_conds = IntMap.empty
+    ; eq_conds = TSet.empty
+    ; chk_conds = CHKSet.empty }
 
   (** [is_empty pool] tells whether the pool of constraints is empty. *)
   let is_empty : t -> bool = fun pool ->
-    PSet.is_empty pool.nl_conds && IntMap.is_empty pool.fv_conds
+    PSet.is_empty pool.nl_conds
+    && IntMap.is_empty pool.fv_conds
+    && TSet.is_empty pool.eq_conds
+    && CHKSet.is_empty pool.chk_conds
 
   (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot]
       in the [vars] array correspond to a term stored at index [i] in the
@@ -119,6 +143,24 @@ module CP = struct
   let register_fv : int -> int array -> t -> t = fun i vs pool ->
     { pool with fv_conds = IntMap.add i vs pool.fv_conds }
 
+  (** [register_eq t1 t2 pool] registers a convertibility constraint
+      between terms [t1] and [t2] in [pool]. *)
+  let register_eq : (psym * int list) -> (psym * int list) -> t -> t =
+    fun (s1,a1) (s2,a2) pool ->
+    let pv1 = List.map (fun i -> IntMap.find i pool.variables) a1 in
+    let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in
+    { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds }
+
+  let register_chk : sym -> r_term list -> t -> t = fun op args pool ->
+    let sy2sy sy = (sy.sym_path, sy.sym_name) in
+    let rec rt2ct t = match t with
+      | R_App (s, al) -> C_App(sy2sy s, List.map rt2ct al)
+      | R_Patt i -> C_Patt (IntMap.find i pool.variables)
+      | R_Sym s -> C_Sym (sy2sy s)
+    in
+    { pool with chk_conds = CHKSet.add (sy2sy op, List.map rt2ct args)
+                              pool.chk_conds }
+
   (** [constrained_nl i pool] tells whether index [i] in the RHS's environment
       has already been associated to a variable of the [vars] array. *)
   let constrained_nl : int -> t -> bool = fun slot pool ->
@@ -129,6 +171,9 @@ module CP = struct
   let is_contained : tree_cond -> t -> bool = fun cond pool ->
     match cond with
     | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds
+    | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds
+                       || TSet.mem (t2,t1) pool.eq_conds
+    | CondCHK(s,al) -> CHKSet.mem (s,al) pool.chk_conds
     | CondFV(i,x) ->
         try Array.eq (=) x (IntMap.find i pool.fv_conds)
         with Not_found -> false
@@ -137,6 +182,9 @@ module CP = struct
   let remove cond pool =
     match cond with
     | CondNL(i,j)  -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds}
+    | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds}
+    | CondCHK(s,al) ->
+        {pool with chk_conds = CHKSet.remove (s,al) pool.chk_conds}
     | CondFV(i,xs) ->
         try
           let ys = IntMap.find i pool.fv_conds in
@@ -161,8 +209,28 @@ module CP = struct
       | p :: ps -> try Some(export (IntMap.choose p.fv_conds))
                    with Not_found -> choose_vf ps
     in
+    let rec choose_eq pools =
+      let export (t1, t2) = CondEQ(t1,t2) in
+      match pools with
+      | []      -> None
+      | p :: ps -> try Some(export (TSet.choose p.eq_conds))
+                   with Not_found -> choose_eq ps
+    in
+    let rec choose_chk pools =
+      let export (op, al) = CondCHK(op,al) in
+      match pools with
+      | []      -> None
+      | p :: ps -> try Some(export (CHKSet.choose p.chk_conds))
+                   with Not_found -> choose_chk ps
+    in
     let res = choose_nl pools in
-    if res = None then choose_vf pools else res
+    if res = None then
+      let res = choose_eq pools in
+      if res = None then
+        let res = choose_chk pools in
+        if res = None then choose_vf pools else res
+      else res
+    else res
 end
 
 (** {1 Clause matrix and pattern matching problem} *)
@@ -196,6 +264,7 @@ module CM = struct
         | Abst _, _ -> "λ"
         | Prod _, _ -> "Π"
         | Type, _   -> "TYPE"
+        | Appl _, _ -> "@"
         | _ -> assert false (* Terms that souldn't appear in lhs *) )
 
   (** Representation of a subterm in argument position in a pattern. *)
@@ -218,12 +287,23 @@ module CM = struct
       [0] index is used when going under abstractions. In that case, the field
       [arg_rank] is incremented. *)
 
+  (** rule constraints *)
+  type c_constraint =
+    | C_EQ of (psym * int list) * (psym * int list)
+    (** convertibility between flat terms *)
+    | C_CHK of psym * c_term list
+    (** predefined constraint between terms *)
+    | C_None
+    (** no cnostraint *)
+
   (** A clause matrix row (schematically {i c_lhs ↪ c_rhs if cond_pool}). *)
   type clause =
     { c_lhs       : term array
     (** Left hand side of a rule. *)
     ; c_rhs       : rule
     (** Right hand side of a rule, and number of extra variables. *)
+    ; c_when      : c_constraint
+    (** constraints for conditional rules *)
     ; c_subst     : rhs_substit
     (** Substitution of RHS variables. *)
     ; xvars_nb    : int
@@ -290,9 +370,21 @@ module CM = struct
 
   (** [of_rules rs] transforms rewriting rules [rs] into a clause matrix. *)
   let of_rules : rule list -> t = fun rs ->
-    let r2r ({lhs; xvars_nb; _} as c_rhs) =
+    let sy2sy s = (s.sym_path,s.sym_name) in
+    let rec rt2ct : r_term -> c_term = fun t ->
+      match t with
+      | R_App(s,tl) -> C_App (sy2sy s, List.map rt2ct tl)
+      | R_Patt i -> C_Patt (i,[||])
+      | R_Sym s -> C_Sym (sy2sy s)
+    in
+    let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) =
       let c_lhs = Array.of_list lhs in
-      { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb }
+      let c_when = match r_when with
+        | R_None -> C_None
+        | R_EQ ((s1,a1),(s2,a2)) -> C_EQ ((sy2sy s1, a1), (sy2sy s2, a2))
+        | R_CHK (f,al) -> C_CHK (sy2sy f, List.map rt2ct al)
+      in
+      { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when }
     in
     let size = (* Get length of longest rule *)
       if rs = [] then 0 else
@@ -357,7 +449,7 @@ module CM = struct
   (** [is_exhausted p c] tells whether clause [r] whose terms are at positions
       in [p] can be applied or not. *)
   let is_exhausted : arg list -> clause -> bool =
-    fun positions {c_lhs = lhs ; cond_pool ; _} ->
+    fun positions {c_lhs = lhs ; cond_pool ; c_when; _} ->
     let nonl lhs =
       (* Verify that there are no non linearity constraints in the remaining
          terms.  We must check that there are no constraints in the remaining
@@ -373,6 +465,7 @@ module CM = struct
     let depths = Array.of_list (List.map (fun i -> i.arg_rank) positions) in
     let ripe lhs =
       (* [ripe l] returns whether [lhs] can be applied. *)
+      Array.length lhs <= Array.length depths && (* jpb *)
       let de = Array.sub depths 0 (Array.length lhs) in
       let check pt de =
       (* We verify that there are no variable constraints, that is, if
@@ -384,7 +477,7 @@ module CM = struct
       in
       Array.for_all2 check lhs de && nonl lhs
     in
-    CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
+    c_when = C_None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
 
   (** [yield m] returns the next operation to carry out on matrix [m], that
       is, either specialising, solving a constraint or rewriting to a rule. *)
@@ -482,6 +575,44 @@ module CM = struct
               CP.register_nl i (mem,vs) cond_pool
           | None    -> cond_pool
         in
+        let c_when, cond_pool =
+          let vars = cond_pool.variables in
+          match r.c_rhs.r_when with
+          | R_None -> r.c_when, cond_pool
+          (* find_doubles ty! op! n! t! d? before? middle? after? *)
+          | R_CHK ({sym_name="#find_doubles";_} as sy,
+                   ([ty; R_App (_, []);u;t;rd;rb;rm;ra] as al)) when
+                 rAll (fun i -> IntMap.mem i vars) ty
+                 && rAll (fun i -> IntMap.mem i vars) u
+                 && rAll (fun i -> IntMap.mem i vars) t -> begin
+              let (_mem, cond_pool) = List.fold_left (rFold (fun (m,p) i -> m+1,CP.register_nl i (m,vs) p))
+                                        (mem,cond_pool) [rd;rb;rm;ra] in
+(*
+              match List.find_map (rFind (fun i -> if IntMap.mem i vars then None else Some i)) [rd;rb;rm;ra] with
+                Some i -> r.c_when, CP.register_nl i (mem,vs) cond_pool
+              | None ->
+*)
+              if Logger.log_enabled () then
+                log "Registering predefined constraint on position [%a] \
+                     %a %a"
+                  arg_path a.arg_path Raw.sym sy (List.pp r_term " ") al;
+                  C_None, CP.register_chk sy al cond_pool
+            end
+          | R_EQ ((op1,a1), (op2,a2)) when
+                 List.for_all (fun i -> IntMap.mem i vars) a1
+                 && List.for_all (fun i -> IntMap.mem i vars) a2 ->
+              if Logger.log_enabled () then
+                log "Registering user constraint on position [%a] \
+                     %s %a == %s %a"
+                  arg_path a.arg_path
+                  op1.sym_name (List.pp int " ") a1
+                  op2.sym_name (List.pp int " ") a2;
+              C_None, CP.register_eq
+                      ((op1.sym_path,op1.sym_name), a1)
+                      ((op2.sym_path,op2.sym_name), a2)
+                      cond_pool
+          | _ -> r.c_when, cond_pool
+        in
         let c_subst =
           (* REVIEW: patterns may have slots in the RHS although they are not
              bound. *)
@@ -499,7 +630,7 @@ module CM = struct
               (mem, (i,vs)) :: r.c_subst
           | _ -> r.c_subst
         in
-        {r with c_subst; cond_pool}
+        {r with c_subst; cond_pool; c_when}
     | _ -> r
 
   (** [specialize free_vars pat col pos cls] filters and transforms LHS of
@@ -670,7 +801,7 @@ let harvest :
         in
         default_node true (loop ts subst (slot + 1))
     | Patt(None,_,_)::ts    -> default_node false (loop ts subst slot)
-    | _                     -> assert false
+    | t :: _ -> log "tree error %a" CM.head t; assert false
   in
   loop (Array.to_list lhs) subst slot
 
@@ -724,7 +855,7 @@ let compile : match_strat -> CM.t -> tree = fun mstrat m ->
       in
       let right = compile_cv {cm with clauses=CM.not_empty_stack clauses} in
       Eos(left, right)
-  | Specialise(swap)                       ->
+  | Specialise(swap) ->
       if Logger.log_enabled () then log "Swap on column %d" swap;
       let store = CM.store cm swap in
       let updated =
diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml
index c2d7d17a2..49a460f8f 100644
--- a/src/core/tree_type.ml
+++ b/src/core/tree_type.ml
@@ -6,6 +6,17 @@ open Common
 (** {3 Atomic pattern constructor representation} *)
 
 type pvar = int * int array
+type psym = Path.t * string
+type c_term =
+  | C_App of psym * c_term list  (* application *)
+  | C_Patt of pvar               (* pattern variable *)
+  | C_Sym of psym                (* global symbol *)
+
+let rec c_term : c_term pp = fun ppf t ->
+  match t with
+  | C_App(s,al) -> out ppf "%s [%a]" (snd s) (List.pp c_term ",") al
+  | C_Patt (i,_) -> out ppf "?%d" i
+  | C_Sym s -> out ppf "%s" (snd s)
 
 (** Representation of an atomic pattern constructor. *)
 module TC =
@@ -56,6 +67,10 @@ type tree_cond =
   | CondFV of pvar
   (** Are the (indexed) bound variables (which are free at the time of the
       checking) of the term at the given index in the array? *)
+  | CondEQ of (psym * pvar list) * (psym * pvar list)
+  (** user rule condition: are the two terms equivalent *)
+  | CondCHK of psym * c_term list
+  (** user rule predefined condition *)
 
 (** {b NOTE} that when performing a [tree_cond.CondFV] check, we
     are concerned about variables that were bound in the term being reduced
@@ -69,6 +84,11 @@ let tree_cond : tree_cond pp = fun ppf tc ->
       out ppf "Nl(%d[%a],%d[%a])"
         i (Array.pp int ",") xs j (Array.pp int ",") ys
   | CondFV(i, _) -> out ppf "Fv(%d)" i
+  | CondEQ((s1,a1), (s2,a2)) ->
+      out ppf "Eq(%s(%a),%s(%a))"
+        (snd s1) (List.pp int ",") (List.map fst a1)
+        (snd s2) (List.pp int ",") (List.map fst a2)
+  | CondCHK(op,al) -> out ppf "CHK %s[%a]" (snd op) (List.pp c_term " ") al
 
 (** Substitution of variables in a RHS. During the filtering process, some
     subterms of the filtered term may be stored in an array. Let [v] be that
diff --git a/src/core/unif.ml b/src/core/unif.ml
index 9f88fcf8f..e8118b8a2 100644
--- a/src/core/unif.ml
+++ b/src/core/unif.ml
@@ -63,7 +63,9 @@ let rec type_app : ctxt -> term -> term list -> term option = fun c a ts ->
   | _, [] -> Some a
   | Prod(_,b), t::ts -> type_app c (subst b t) ts
   | LLet(_,d,b), t::ts ->
-      assert (Eval.pure_eq_modulo c d t); type_app c (subst b d) ts
+let _ = if not (Eval.pure_eq_modulo c d t) then
+log "LET ERROR??? %a -- %a" term a term t in
+      (*assert (Eval.pure_eq_modulo c d t);*) type_app c (subst b d) ts
   | _ ->
       match Eval.whnf c a, ts with
       | Prod(_,b), t::ts -> type_app c (subst b t) ts
diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml
index 2a874003d..3935cdb91 100644
--- a/src/export/rawdk.ml
+++ b/src/export/rawdk.ml
@@ -135,9 +135,12 @@ let rec remove_wraps ({elt;_} as t) =
 
 let rule : p_rule pp =
   let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in
-  fun ppf {elt=(l,r);_} ->
-  out ppf "[%a] %a --> %a.@."
-    varset (pvars_lhs l) term (remove_wraps l) term r
+  fun ppf {elt=(l,r,w);_} ->
+  if w = P_None then
+    out ppf "[%a] %a --> %a.@."
+      varset (pvars_lhs l) term (remove_wraps l) term r
+  else
+    fatal None "Cannot translate conditional rules."
 
 type modifiers
   = prop list * expo list * match_strat list * p_modifier_aux list
diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml
index 4abb54694..c05d6b473 100644
--- a/src/handle/inductive.ml
+++ b/src/handle/inductive.ml
@@ -347,7 +347,7 @@ let iter_rec_rules :
     let nonrec_dom _ _ next = next in
     let codom xs rhs _ ts =
       let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in
-      Pos.make rule_pos (arec ind_sym ts cons_arg, rhs)
+      Pos.make rule_pos (arec ind_sym ts cons_arg, rhs, P_None)
     in
     fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var
       init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom
diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
index daf2e0076..f764f2c3d 100644
--- a/src/handle/tactic.ml
+++ b/src/handle/tactic.ml
@@ -109,6 +109,7 @@ let tac_solve : popt -> proof_state -> proof_state = fun pos ps ->
     gs_typ @ MetaSet.fold add_goal (!p).metas
                (List.map (fun c -> Unif c) (!p).unsolved)
   in
+let _ = log "SOLVE: %a" (List.pp Goal.pp "\n") proof_goals in
   {ps with proof_goals}
 
 (** [tac_refine pos ps gt gs p t] refines the typing goal [gt] with [t]. *)
@@ -794,7 +795,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
           let term = term_in (Ctxt.names c) in
           fatal pt.pos "Cannot infer the type of [%a]" term t
       | Some(t,_) ->
-        if Unif.solve_noexn p then
+        if Unif.solve_noexn p && !p.unsolved = [] then
           let ps, t = p_tactic ps g env pos t in handle ps t
         else fatal pos "Cannot solve typing constraints for [%a]" term t
 
diff --git a/src/parsing/dkRule.ml b/src/parsing/dkRule.ml
index 09d709a20..135420c42 100644
--- a/src/parsing/dkRule.ml
+++ b/src/parsing/dkRule.ml
@@ -155,4 +155,4 @@ let to_p_rule : p_dk_rule -> p_rule = fun r ->
   (* NOTE the computation order is important for setting arities properly. *)
   let lhs = build [] lhs in
   let rhs = build [] rhs in
-  Pos.make r.pos (lhs, rhs)
+  Pos.make r.pos (lhs, rhs, P_None)
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index 7ec7c7616..6b9a24eec 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -100,6 +100,7 @@ type token =
   | TYPE_TERM
   | UNIF_RULE
   | VERBOSE
+  | WHEN
   | WHY3
   | WITH
 
@@ -305,6 +306,7 @@ let rec token ~allow_rocq_syntax lb =
   | "TYPE" -> TYPE_TERM
   | "unif_rule" -> UNIF_RULE
   | "verbose" -> VERBOSE
+  | "when" -> WHEN
   | "why3" -> WHY3
   | "with" -> WITH
 
diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index a43035cc1..eaf5b63f7 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -123,6 +123,7 @@ let string_of_token =
   | UNIF_RULE -> q"unif_rule"
   | VBAR -> q"|"
   | VERBOSE -> q"verbose"
+  | WHEN -> q"when"
   | WHY3 -> q"why3"
   | WITH -> q"with"
 
@@ -633,7 +634,7 @@ and command (lb:'token lexbuf) : p_command =
         let (en, es) = List.(hd es, tl es) in
         let cat e es = P.appl (P.appl cons e) es in
         let rhs = List.fold_right cat es en in
-        let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs) in
+        let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, P_None) in
         extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r))
     | COERCE_RULE ->
         consume_token lb;
@@ -784,13 +785,27 @@ and notation (lb:'token lexbuf): string Term.notation =
       expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER]
 
 and rule_tks () = term_tks
-and rule (lb:'token lexbuf): (p_term * p_term) loc =
+and rule (lb:'token lexbuf):
+      (p_term * p_term * p_constraint) loc =
   if log_enabled() then log "%s" __FUNCTION__;
   let pos1 = current_pos lb in
   let l = term lb in
+  let w =
+    if (current_token lb == WHEN) then begin
+        consume WHEN lb;
+        let t1 = term lb in
+        if (current_token lb == EQUIV) then begin
+            consume EQUIV lb;
+            let t2 = term lb in
+            P_EQ(t1, t2)
+          end
+        else
+          P_CHK t1
+      end
+    else P_None in
   consume HOOK_ARROW lb;
   let r = term lb in
-  extend_pos lb (*__FUNCTION__*) pos1 (l, r)
+  extend_pos lb (*__FUNCTION__*) pos1 (l, r, w)
 
 and equation_tks () = term_tks
 and equation (lb:'token lexbuf): p_term * p_term =
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index c39218c84..8f2f37091 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -187,8 +187,12 @@ and params_list : p_params list pp = fun ppf ->
 and typ : p_term option pp = fun ppf t ->
   Option.iter (out ppf "@ : %a" term) t
 
-let rule : string -> p_rule pp = fun kw ppf {elt=(l,r);_} ->
-  out ppf "%s %a ↪ %a" kw term l term r
+let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} ->
+  match w with
+  | P_None -> out ppf "%s %a ↪ %a" kw term l term r
+  | P_EQ (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a"
+                      kw term l term t1 term t2 term r
+  | P_CHK t -> out ppf "%s %a when %a ↪ %a" kw term l term t term r
 
 let inductive : string -> p_inductive pp =
   let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in
@@ -214,7 +218,7 @@ let rec unpack : p_term -> (p_term * p_term) list = fun eqs ->
       else assert false
   | _ -> assert false
 
-let unif_rule : p_rule pp = fun ppf {elt=(l,r);_} ->
+let unif_rule : p_rule pp = fun ppf {elt=(l,r,_);_} ->
   let lhs =
     match Syntax.p_get_args l with
     | (_, [t; u]) -> (t, u)
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index a973f4163..973888b32 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -554,11 +554,26 @@ let patt_vars : p_term -> (string * int) list * string list =
 let scope_rule :
   ?find_sym:find_sym -> bool -> sig_state -> p_rule -> sym_rule =
   fun ?(find_sym=Sig_state.find_sym) ur ss
-      { elt = (p_lhs, p_rhs); pos = rule_pos} ->
+      { elt = (p_lhs, p_rhs, p_when); pos = rule_pos} ->
   (* Compute the set of pattern variables on both sides. *)
   let (pvs_lhs, nl) = patt_vars p_lhs in
   (* NOTE to reject non-left-linear rules check [nl = []] here. *)
   let (pvs_rhs, _ ) = patt_vars p_rhs in
+  (* input/output variables in condition *)
+  let pvs_when =
+    match p_when with
+    | P_None -> [],[]
+    | P_EQ (t1,t2) ->
+        let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in
+        (p1 @ p2), []
+    | P_CHK t -> 
+        match p_get_args t with
+          (* find_doubles op! n! t! d? before? middle? after? *)
+        | {elt=P_Iden({elt=(_,"#find_doubles");_},_);_}, [ty;op;u;t;d;b;m;a] ->
+            (List.concat_map (fun t -> fst (patt_vars t)) [ty;u;t]),
+            (List.concat_map (fun t -> fst (patt_vars t)) [d;b;m;a])
+        | _ -> fatal t.pos "Undefined constraint."
+  in
   (* Check that pattern variables of RHS that are in the LHS have the right
      arity. *)
   let check_arity (m,i) =
@@ -568,6 +583,8 @@ let scope_rule :
     with Not_found -> ()
   in
   List.iter check_arity pvs_rhs;
+  List.iter check_arity (fst pvs_when);
+  List.iter check_arity (snd pvs_when);
   (* [get_root t] returns the symbol at the root of the p_term [t]. *)
   let rec get_root t = get_root_after_pratt (Pratt.parse ~find_sym ss [] t)
   and get_root_after_pratt t =
@@ -599,9 +616,13 @@ let scope_rule :
            ; m_lhs_arities = Hashtbl.create 7
            ; m_lhs_names   = Hashtbl.create 7
            ; m_lhs_size    = 0
-           ; m_lhs_in_env  = nl @ List.map fst pvs_rhs }
+           ; m_lhs_in_env  =
+               nl @ List.map fst pvs_rhs @ List.map fst (snd pvs_when)}
     in
     let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in
+    let _ = match p_when with
+        P_CHK t -> ignore (scope ~find_sym 0 mode ss Env.empty t)
+      | _ -> () in
     match mode with
     | M_LHS{ m_lhs_indices; m_lhs_names; m_lhs_size; m_lhs_arities; _} ->
       let lhs = snd (get_args lhs) in
@@ -630,7 +651,40 @@ let scope_rule :
   let arity = List.length lhs in
   let f i = try Hashtbl.find names i with Not_found -> string_of_int i in
   let names = Array.init vars_nb f in
-  let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; rule_pos} in
+  let asPatt t = match unfold t with
+    | Patt (Some i, _, [||]) -> i
+    | _ -> fatal rule_pos "arguments should be patterns in condition [%a]."
+             term t in
+  let rec asRTerm: Term.term -> Term.r_term = fun t ->
+    match get_args t with
+    | Patt (Some i, _, [||]), [] -> R_Patt i
+    | Patt (None, _, _), _ ->
+        fatal rule_pos "anonymous pattern not allowed in constraint [%a]."
+          term t
+    | Patt _, _ ->
+        fatal rule_pos "pattern applicationn not allowed in constraint [%a]."
+          term t
+    | Symb s, tl -> R_App (s, List.map asRTerm tl)
+    | f,_ -> fatal rule_pos "Not allowed in constraint [%a]."
+               term f in
+  let asRTerm : Term.term -> sym * Term.r_term list = fun t ->
+    match asRTerm t with
+    | R_App (s,al) -> s,al
+    | _ -> fatal rule_pos "constraint should be a function call [%a]."
+             term t in
+  let p_asRTerm t = asRTerm (scope ~find_sym 0 mode ss Env.empty t) in
+  let pw2rw t =
+    let t = scope ~find_sym 0 mode ss Env.empty t in
+    match get_args t with
+      Symb s, args ->  (s, List.map asPatt args)
+    | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t
+  in
+  let r_when = match p_when with
+    | P_None -> R_None
+    | P_EQ (t1,t2) -> R_EQ (pw2rw t1, pw2rw t2)
+    | P_CHK t -> let (f,al) = p_asRTerm t in R_CHK (f,al) in
+  let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb;
+           rule_pos; r_when} in
   (sym,r)
 
 (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index 2e1e096ec..478f31fdf 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -133,8 +133,13 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} ->
   | P_Expl u
     -> pvars_lhs u
 
+type p_constraint =
+  P_EQ of p_term * p_term           (* when t1 == t2 *)
+| P_CHK of p_term  (* when t *)
+| P_None
+
 (** Parser-level rewriting rule representation. *)
-type p_rule_aux = p_term * p_term
+type p_rule_aux = p_term * p_term * p_constraint
 type p_rule = p_rule_aux loc
 
 (** Parser-level inductive type representation. *)
@@ -182,7 +187,8 @@ module P  = struct
   let abst_list : p_ident option list -> p_term -> p_term = fun idopts t ->
     List.fold_right abst idopts t
 
-  let rule : p_term -> p_term -> p_rule = fun l r -> Pos.none (l,r)
+  let rule : p_term -> p_term -> p_constraint -> p_rule =
+    fun l r w -> Pos.none (l,r,w)
 end
 
 (** Rewrite patterns as in Coq/SSReflect. See "A Small Scale
@@ -499,8 +505,20 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) ->
   List.eq (Option.eq eq_p_ident) i1 i2
   && Option.eq eq_p_term ao1 ao2 && b1 = b2
 
-let eq_p_rule : p_rule eq = fun {elt=(l1,r1);_} {elt=(l2,r2);_} ->
-  eq_p_term l1 l2 && eq_p_term r1 r2
+let eq_p_constraint: p_constraint eq = fun c1 c2 ->
+  match c1,c2 with
+    P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2
+  | P_CHK t1, P_CHK t2 -> eq_p_term t1 t2
+  | P_None, P_None -> true
+  | _ -> false
+
+let pair_eq: 'a eq -> 'b eq -> ('a * 'b) eq = fun eq1 eq2 (x1,y1) (x2,y2) ->
+  eq1 x1 x2 && eq2 y1 y2
+
+let eq_p_rule : p_rule eq = fun {elt=(l1,r1,w1);_} {elt=(l2,r2,w2);_} ->
+  eq_p_term l1 l2
+  && eq_p_term r1 r2
+  && eq_p_constraint w1 w2
 
 let eq_p_inductive : p_inductive eq =
   let eq_cons (i1,t1) (i2,t2) = eq_p_ident i1 i2 && eq_p_term t1 t2 in
@@ -716,8 +734,15 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
 
   let fold_term : 'a -> p_term -> 'a = fold_term_vars StrSet.empty in
 
-  let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r);_} ->
-    fold_term (fold_term a l) r
+  let fold_constraint : 'a -> p_constraint -> 'a = fun a w ->
+    match w with
+    | P_EQ (t1,t2) -> fold_term (fold_term a t1) t2
+    | P_CHK t -> fold_term a t
+    | P_None -> a
+  in
+
+  let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r,w);_} ->
+    fold_constraint (fold_term (fold_term a l) r) w
   in
 
   let fold_rwpatt_vars : StrSet.t -> 'a -> p_rwpatt -> 'a = fun vs a p ->
diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml
index 950044fac..2a60412ce 100644
--- a/src/tool/lcr.ml
+++ b/src/tool/lcr.ml
@@ -55,7 +55,7 @@ let is_definable : sym -> bool = fun s ->
 (** [rule_of_def s d] creates the rule [s --> d]. *)
 let rule_of_def : sym -> term -> rule = fun s rhs ->
   {lhs=[]; names=[||]; rhs; arity=0; arities=[||]; vars_nb=0; xvars_nb=0;
-   rule_pos=s.sym_pos}
+   rule_pos=s.sym_pos; r_when = R_None}
 
 (** [replace t p u] replaces the subterm of [t] at position [p] by [u]. *)
 let replace : term -> subterm_pos -> term -> term = fun t p u ->
@@ -445,7 +445,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t ->
     match get_args_len l with
     | Symb s, lhs, arity ->
       let r = {lhs; names=[||]; rhs; arity; arities=[||]; vars_nb=0;
-               xvars_nb=0; rule_pos=Some(new_rule_id())} in
+               xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = R_None} in
       Some (s,r)
     | _ -> None
   in
diff --git a/src/tool/sr.ml b/src/tool/sr.ml
index eaf9b520c..43e258430 100644
--- a/src/tool/sr.ml
+++ b/src/tool/sr.ml
@@ -83,6 +83,29 @@ let symb_to_patt : Pos.popt -> (int * int option) SymMap.t -> string array
   in
   symb_to_patt
 
+(** [check_constraint p metas c] adds typing constraints associated to 
+    rule condition [c] to [p] after replacing variable indexes by metas 
+    variables in [c]. *)
+let check_constraint : 
+      problem -> meta array -> r_constraint -> 
+      (term * term) option
+  = fun p metas c ->
+  let rec asTerm : r_term -> term = fun t ->
+    match t with
+    | R_App(sy,al) ->
+        List.fold_left (fun f a -> mk_Appl(f,asTerm a)) (mk_Symb sy) al
+    | R_Patt i -> mk_Meta (metas.(i),[||])
+    | R_Sym sy -> mk_Symb sy in
+  match c with
+  | R_EQ ((sy1,al1),(sy2,al2)) -> 
+      let t1 = asTerm (R_App(sy1, List.map (fun i -> R_Patt i) al1)) in
+      let t2 = asTerm (R_App(sy2, List.map (fun i -> R_Patt i) al2)) in
+      let t = add_args (mk_Symb Unif_rule.equiv) [t1;t2] in
+      Infer.infer_noexn p [] t
+  | R_CHK (sy, al) ->
+      Infer.infer_noexn p [] (asTerm (R_App(sy,al)))
+  | R_None -> Infer.infer_noexn p [] mk_Type
+
 (** [check_rule r] checks whether the rule [r] preserves typing. *)
 let check_rule : Pos.popt -> sym_rule -> sym_rule =
   fun pos ((s,({lhs;names;rhs;arities;vars_nb;xvars_nb;_} as r)) as sr) ->
@@ -121,6 +144,13 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
   | Some (lhs_with_metas, ty_lhs) ->
   if not (Unif.solve_noexn ~type_check:false p) then
     fatal pos "The LHS is not typable.";
+  (* Infer the typing constraints of the condition. *)
+  match check_constraint p metas r.r_when with
+  | None -> fatal pos "The constraint is not typable."
+  | Some (_,_) -> 
+  if not (Unif.solve_noexn ~type_check:false p) then
+    fatal pos "The constraint is not typable.";
+  (* Try to simplify constraints. *)
   (* Normalize constraints. *)
   let norm_constr (c,t,u) = (c, Eval.snf [] t, Eval.snf [] u) in
   let lhs_constrs = List.map norm_constr !p.unsolved in
diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml
index 3097edf56..cbab95dfc 100644
--- a/src/tool/tree_graphviz.ml
+++ b/src/tool/tree_graphviz.ml
@@ -46,6 +46,11 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree ->
       | CondNL((i,vi), (j,vj)) ->
           out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj
       | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i
+      | CondCHK(op,al) -> out ppf "%s[%a]" (snd op) (List.pp c_term ",") al
+      | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) ->
+          out ppf "%s[%a] ≡ %s[%a]"
+            s1 (List.pp int ",") (List.map fst a1)
+            s2 (List.pp int ",") (List.map fst a2)
     in
     let node_count = ref 0 in
     (* [write_tree n u v] writes tree [v] obtained from tree number [n] with a
diff --git a/tests/OK/cond_rules.lp b/tests/OK/cond_rules.lp
new file mode 100644
index 000000000..0402de7e0
--- /dev/null
+++ b/tests/OK/cond_rules.lp
@@ -0,0 +1,20 @@
+symbol Prop: TYPE;
+symbol ∧: Prop → Prop → Prop;
+notation ∧ infix right 7;
+constant symbol ⊤ : Prop;
+constant symbol ⊥ : Prop;
+
+sequential symbol doubles_in_and : Prop → Prop;
+sequential symbol occurs_in_and : Prop → Prop → Prop;
+
+rule doubles_in_and ($p ∧ $q) when occurs_in_and $p $q ≡ ⊤ ↪ ⊤
+with doubles_in_and (_ ∧ $q) ↪ doubles_in_and $q
+with doubles_in_and _ ↪ ⊥;
+
+rule occurs_in_and $p $p ↪ ⊤
+with occurs_in_and $p ($p ∧ _) ↪ ⊤
+with occurs_in_and $p (_ ∧ $q) ↪ occurs_in_and $p $q
+with occurs_in_and _ _ ↪ ⊥;
+
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥;
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ p ∧ r) ≡ ⊤;
diff --git a/tests/OK/cond_rules_st.lp b/tests/OK/cond_rules_st.lp
new file mode 100644
index 000000000..c9aa5a6fd
--- /dev/null
+++ b/tests/OK/cond_rules_st.lp
@@ -0,0 +1,20 @@
+require open tests.OK.List;
+
+symbol ∧: Prop → Prop → Prop;
+notation ∧ infix right 7;
+constant symbol ⊤ : Prop;
+constant symbol ⊥ : Prop;
+
+constant symbol o: Set;
+rule τ o ↪ Prop;
+
+symbol #find_doubles (T:Set) (op: τ T → τ T → τ T) (u: τ T) (p: τ T) (d: τ T) (b m a: τ T): Prop;
+
+sequential symbol simpl: Prop → Prop;
+rule simpl $p when #find_doubles o @∧ ⊤ $p $d $b $m $a ↪ $b ∧ $d ∧ $m ∧ $a;
+rule simpl $p ↪ $p;
+
+//compute (λ p q r, simpl (p ∧ q ∧ r ∧ p));
+
+//assert p q r ⊢ simpl (p ∧ q ∧ r) ≡ p ∧ q ∧ r;
+assert p q r ⊢ simpl (q ∧ p ∧ r ∧ p) ≡ p;
diff --git a/tests/export_dk.sh b/tests/export_dk.sh
index 741967625..d53991647 100755
--- a/tests/export_dk.sh
+++ b/tests/export_dk.sh
@@ -49,6 +49,8 @@ do
         Tactic|1374);;
         # use Tactic
         first_hyp|all_hyps);;
+        # use cond rules
+        cond_rules*);;
         # requires an excluded file
         assume|first_hyp);;
         # default case
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index 24aceb8f3..3ba49c799 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -58,6 +58,8 @@ do
         require_nondkmident);;
         # module alias
         alias);;
+        # conditional rules
+        cond_rules*);;
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps);;
         # "open"