diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-25 18:07:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-25 18:07:06 +0000 |
| commit | a638cba857c9a93a62f35bcceab6fa2c710805d2 (patch) | |
| tree | d6ca6ede23703333e34058b8113f5ef521583891 | |
| parent | 85dae158c3225dc0dde6762e50f6fdef2203fdd5 (diff) | |
Polishing commits r14492, r14448 and r14407 (tactics propagate
conversion hints to kernel). Whether REVERTcast must be known from
coqchk is unclear. In the meantime, warn about the unstability of the
situation (see also bug #2599).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14495 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | kernel/term.ml | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 278fdb399..3fc90761d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -160,6 +160,7 @@ let cast_kind_display k = match k with | VMcast -> "VMcast" | DEFAULTcast -> "DEFAULTcast" + | REVERTcast -> "REVERTcast" let constr_display csr = let rec term_display c = match kind_of_term c with diff --git a/kernel/term.ml b/kernel/term.ml index 1ed918519..a6519e226 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -34,6 +34,8 @@ type existential_key = int type metavariable = int (* This defines the strategy to use for verifiying a Cast *) +(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *) +(* come after the vo-exported cast_kind so as to be compatible with coqchk *) type cast_kind = VMcast | DEFAULTcast | REVERTcast (* This defines Cases annotations *) |