diff options
Diffstat (limited to 'parsing/coqlib.mli')
| -rw-r--r-- | parsing/coqlib.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli index dc65d7ab8..0b5bb0ec5 100644 --- a/parsing/coqlib.mli +++ b/parsing/coqlib.mli @@ -29,9 +29,6 @@ val glob_nat : global_reference val glob_O : global_reference val glob_S : global_reference -(* Special variable for pretty-printing of constant naturals *) -val glob_My_special_variable_nat : global_reference - (* Equality *) val glob_eq : global_reference val glob_eqT : global_reference @@ -129,12 +126,5 @@ val build_coq_eqdec_partial_pattern : constr_pattern delayed (* ["! (x,y:?1). (sumbool (eq ?1 x y) ~(eq ?1 x y))"] *) val build_coq_eqdec_pattern : constr_pattern delayed -(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *) -val build_coq_refl_rel1_pattern : constr_pattern delayed -val build_coq_refl_rel2_pattern : constr_pattern delayed - -(* ["(?1 -> ?2)"] *) -val build_coq_arrow_pattern : constr_pattern delayed - (* ["(sig ?1 ?2)"] *) val build_coq_sig_pattern : constr_pattern delayed |