diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 new file mode 100644 index 00000000..34348834 --- /dev/null +++ b/tactics/extraargs.ml4 @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id: extraargs.ml4,v 1.5.2.1 2004/07/16 19:30:53 herbelin Exp $ *) + +open Pp +open Pcoq +open Genarg + +(* Rewriting orientation *) + +let _ = Metasyntax.add_token_obj "<-" +let _ = Metasyntax.add_token_obj "->" + +let pr_orient _prc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" + +ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient +| [ "->" ] -> [ true ] +| [ "<-" ] -> [ false ] +| [ ] -> [ true ] +END + |