Commit fde14c43 authored by Martin Clochard's avatar Martin Clochard

WIP: new term matching engine (to be integrated in compute)

parent aa1f92c5
......@@ -202,7 +202,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \
prop_curry eliminate_literal \
generic_arg_trans_utils case apply \
ind_itp destruct cut \
induction induction_pr
induction induction_pr matching
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
pvs isabelle \
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment