snapshot

[helm.git] / helm / ocaml / cic_notation / doc / samples.ma

diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma
index abd8b7866685aeeb4df42298a916320791def675..d724ac4eb7a340c6821ff1af491cf3a1bf424b4d 100644 (file)
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -25,6 +25,7 @@ interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 
+notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
 interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)).
 render cic:/Coq/Arith/Plus/plus_comm.con.