From 27ea35bafdf0aefe1dcf49dfed1a18c3f158efa5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Apr 2007 13:56:03 +0000
Subject: Ajout de la possibilité de faire référence dans certains cas à un nom
 par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7.
 unfold "+".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pptactic.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing/pptactic.mli')

diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 993f1ae622..cfa035b169 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -21,6 +21,7 @@ open Environ
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
 val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
 val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) -> 
-- 
cgit v1.2.3