diff options
| author | msozeau | 2007-01-02 16:19:21 +0000 |
|---|---|---|
| committer | msozeau | 2007-01-02 16:19:21 +0000 |
| commit | fa072a140016af98c8a4a771a55217adf9a8f2b3 (patch) | |
| tree | 3c4817a3d8a2798d66f3e0f7d48f48330fdfb077 /pretyping | |
| parent | 0225d6e1fbf24f32908bb3c78cd4ce54c994a1ca (diff) | |
Rework subtac pattern matching equalities generation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9470 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 37667f7417..7fbd130ca4 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -30,6 +30,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds val print_constr_env : env -> constr -> std_ppcmds val print_named_context : env -> std_ppcmds +val pr_rel_decl : env -> rel_declaration -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds |