diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-07 17:01:45 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-07 17:01:45 +0000 |
| commit | 21da23d5a27a1a85f4c55d487b55ae044fe7c555 (patch) | |
| tree | 7e1fc70aaf922d6656d8040021ef1f9cb8b94fdb /dev/include | |
| parent | 923d3d758d112631f664f4c079138dca3c88b189 (diff) | |
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
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/include b/dev/include index b72e68ac0..243f9ea5f 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;; |