amortized de Bruijn instantiation in terms and formulas

c0c56b43 · Andrei Paskevich · 9b41a85e · c0c56b43 · c0c56b43
Commit c0c56b43 authored Jul 20, 2010 by Andrei Paskevich
Expand all Hide whitespace changes
Inline Side-by-side

Showing with 439 additions and 311 deletions

src/core/term.ml src/core/term.ml +438 -310

src/core/term.mli src/core/term.mli +1 -1

No files found.
--- a/src/core/term.ml
+++ b/src/core/term.ml
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -402,7 +402,7 @@ val f_subst_term_alpha : term -> term -> fmla -> fmla
 val t_subst_fmla_alpha : fmla -> fmla -> term -> term
 val f_subst_fmla_alpha : fmla -> fmla -> fmla -> fmla

-(** term/fmla matching modulo alpha in the pattern *)
+(** binder-free term/fmla matching *)

 exception NoMatch