snapshot (added typed environment in 2 -> 1 conversion)

[helm.git] / helm / ocaml / cic_notation / cicNotationTag.ml

diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml
index 67e966823944ade755f73f186bfc07c8a2ccbdd3..336f204b7b32f2d26cd5dadb928b6a64d20bf841 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationTag.ml
+++ b/helm/ocaml/cic_notation/cicNotationTag.ml
@@ -49,10 +49,10 @@ let compatible t1 t2 =
   match t1, t2 with
   | Variable _, Variable _ -> true
   | Variable _, _
-  | _, Variable _ -> false
-  | Layout _, _
-  | _, Layout _
+  | _, Variable _
   | Magic _, _
-  | _, Magic _ -> assert false
+  | _, Magic _ -> false
+  | Layout _, _
+  | _, Layout _ -> assert false
   | _ -> true