ok, but slow on includes

[helm.git] / helm / software / components / ng_tactics / nCicElim.ml

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 9db98de498d99e7e10e2f154d22e9a5f4c723484..d5cbca892e15f045d446e82903dbbdd84106cfdf 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -38,6 +38,7 @@ let mk_appl =
  function
     [] -> assert false
   | [x] -> x
+  | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2)
   | l -> CicNotationPt.Appl l
 ;;