From 7028d08eb6e08d1a1af7f8e99f2e9edd880b8da2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 5 Nov 2015 16:04:59 +0100 Subject: ENH: improving precision --- doc/refman/RefMan-cic.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 148c4505c..f6e9152ca 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1295,7 +1295,7 @@ one corresponds to object $m$. \Coq{} can sometimes infer this predicate but sometimes not. The concrete syntax for describing this predicate uses the \kw{as\ldots in\ldots return} construction. For instance, let us assume that $I$ is an unary predicate with one -parameter. The predicate is made explicit using the syntax: +parameter and one argument. The predicate is made explicit using the syntax: \[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ P ~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~ (c_n~x_{n1}~...~x_{np_n}) \Ra f_n \kw{end}\] -- cgit v1.2.3