From 4c6ce76403035630db684e7c323ae171c4f28de5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 18 Jul 2011 20:41:15 +0000
Subject: Fixed a "feature" of "inversion" and "dependent rewrite" revealed by
 the extension of "dependent rewrite" to "sig" type in r14279: in case of an
 equality "existT a p = x", no rewriting was done at all instead of
 substituting "x" as "inversion" normally does when an equality "x = t" is
 generated.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14287 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 1648d5791c..5d48722732 100644
--- a/dev/include
+++ b/dev/include
@@ -24,6 +24,7 @@
 #install_printer  (* judgement *) ppj;;
 
 #install_printer  (* hint_db *)  print_hint_db;;
+#install_printer  (* Goal.goal *)  ppgoal;;
 #install_printer  (* Goal.goal *)  ppgoalgoal;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
-- 
cgit v1.2.3