parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_unification / cicMetaSubst.mli

diff --git a/helm/software/components/cic_unification/cicMetaSubst.mli b/helm/software/components/cic_unification/cicMetaSubst.mli
index bc5b4c0390b480dc20ee3379713510e9e4a3124b..0d2a08d55223f19f2e50d1446f271813e83e7682 100644 (file)
--- a/helm/software/components/cic_unification/cicMetaSubst.mli
+++ b/helm/software/components/cic_unification/cicMetaSubst.mli
@@ -71,9 +71,6 @@ val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string
 val ppcontext:
  metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context ->
    string
-val ppterm_in_name_context:
- metasenv:Cic.metasenv -> Cic.substitution -> Cic.term ->
-  (Cic.name option) list -> string
 val ppterm_in_context:
  metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string
 val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string