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 | |
| 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')
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 |
2 files changed, 2 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;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 89a6eb5e3..681cb0634 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -114,6 +114,7 @@ let pp_transparent_state s = pp (pr_transparent_state s) let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map evd) let ppclenv clenv = pp(pr_clenv clenv) +let ppgoalgoal gl = pp(Goal.pr_goal gl) (* spiwack: deactivated until a replacement is found let ppgoal g = pp(db_pr_goal g) let pppftreestate p = pp(print_pftreestate p) |