diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-20 23:24:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 16:44:41 +0200 |
| commit | f3515efc26a693f4c525ad91c37c982f4c96e6ec (patch) | |
| tree | 6e74da53a761857bf905b5f43c498b3a4aac0fc0 /ltac/tacentries.ml | |
| parent | 65578a55b81252e2c4b006728522839a9e37cd5c (diff) | |
Factorizing the declaration of ML notation printing in Tacentries.
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 46e48c695..a3e15866e 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -360,7 +360,13 @@ let extend_atomic_tactic name entries = List.iteri add_atomic entries let cache_ml_tactic_notation (_, obj) = - extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod + extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod; + let pp_rule prods = { + Pptactic.pptac_level = 0 (* only level 0 supported here *); + pptac_prods = prods; + } in + let pp_rules = Array.map_of_list pp_rule obj.mltacobj_prod in + Pptactic.declare_ml_tactic_pprule obj.mltacobj_name pp_rules let open_ml_tactic_notation i obj = if Int.equal i 1 then cache_ml_tactic_notation obj |