diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 9ff8ee9ca9..b308b22a4b 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -34,7 +34,7 @@ type existential_key = int type metavariable = int (* This defines the strategy to use for verifiying a Cast *) -type cast_kind = VMcast | DEFAULTcast +type cast_kind = VMcast | DEFAULTcast | REVERTcast (* This defines Cases annotations *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle @@ -135,7 +135,7 @@ let mkSort = function (* (that means t2 is declared as the type of t1) *) let mkCast (t1,k2,t2) = match t1 with - | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2) + | Cast (c,k1, _) when k1 = VMcast & k1 = k2 -> Cast (c,k1,t2) | _ -> Cast (t1,k2,t2) (* Constructs the product (x:t1)t2 *) |