diff options
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 7f2ea95a4..ce3817404 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -254,7 +254,7 @@ vinterp_add "AddDadRule" let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in (add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr (Ctast.ast_to_ct com))) | _ -> errorlabstrm "AddDadRule1" - [< 'sTR "AddDadRule2">]); + [< str "AddDadRule2">]); add_dad_rule "distributivity-inv" (Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) [2; 2] |