diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/interface/dad.ml | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/interface/dad.ml')
| -rw-r--r-- | contrib/interface/dad.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 8096bc31..c2ab2dc8 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -99,7 +99,7 @@ let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = with Failure s -> failwith "internal" in let _, constr_pat = - interp_constrpattern Evd.empty (Global.env()) + intern_constr_pattern Evd.empty (Global.env()) ((*ct_to_ast*) pat) in let subst = matches constr_pat term_to_match in if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then |