From 667de252676eb051fc4e056234f505ebafc335ca Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 9 Feb 2008 10:59:29 +0000
Subject: Fix the clrewrite tactic, change Relations.v to work on relations in
 Prop only, and get rid of the "relation" definition which makes unification
 fail blatantly. Replace it with a notation :) In its current state, the new
 tactic seems ready for larger tests.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-ext.tex | 2 --
 1 file changed, 2 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3a834ff8a8..5dc06f33cc 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1192,8 +1192,6 @@ Check (fun l:list (list nat) => map length l).
 \Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
-\Rem 
-
 \Rem If the list of arguments is empty, the command removes the
 implicit arguments of {\qualid}.
 
-- 
cgit v1.2.3