X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.ml;h=1e721a456bf1d99795ea367d96032e04807ba431;hb=refs%2Ftags%2FPRE_UNIVERSES;hp=7304b39f5c12d99221d27e021e1043155e54f6ef;hpb=0694dd98ca6dbc0c5aa3a1d42a6316b083b3be7c;p=helm.git diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml index 7304b39f5..1e721a456 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -43,7 +43,6 @@ let sort_entries entries = let levels_of_term metasenv context term = let module TC = CicTypeChecker in let module Red = CicReduction in - let module Misc = MQueryMisc in let degree t = let rec degree_aux = function | Cic.Sort _ -> 1