diff options
Diffstat (limited to 'contrib/correctness/pmisc.mli')
| -rw-r--r-- | contrib/correctness/pmisc.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli index 9e32f147eb..393141233a 100644 --- a/contrib/correctness/pmisc.mli +++ b/contrib/correctness/pmisc.mli @@ -53,7 +53,7 @@ val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t val real_subst_in_constr : (identifier * constr) list -> constr -> constr val constant : string -> constr -val coq_constant : string list -> string -> section_path +val coq_constant : string list -> string -> kernel_name val conj : constr -> constr -> constr val coq_true : constr |