From 21da23d5a27a1a85f4c55d487b55ae044fe7c555 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 7 Feb 2011 17:01:45 +0000
Subject: Factorize code of rewrite to make way for a new implementation using
 the new proof engine. Correct treatment of the evar set: the tactic
 incrementally extends (and potentially refines) the existing sigma and the
 internally generated typeclasses constraints are removed from it at the end
 as they are always solved. This avoids tricky and costly evar_map
 manipulations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13812 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 b72e68ac07..243f9ea5f5 100644
--- a/dev/include
+++ b/dev/include
@@ -27,6 +27,7 @@
 #install_printer  (* goal *)  ppgoal;;
 #install_printer  (* sigma goal *)  ppsigmagoal;;
 #install_printer  (* proof *)  pproof;;
+#install_printer  (* Goal.goal *)  ppgoalgoal;;
 #install_printer  (* pftreestate *)  pppftreestate;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
-- 
cgit v1.2.3