diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-30 10:52:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-30 10:52:19 +0000 |
| commit | aa98cbeaa05796ae7bc8a5e4f94954e634695ea0 (patch) | |
| tree | 77dc2fa45a852554b72ecffd6df175eb29742d9a /toplevel/metasyntax.ml | |
| parent | be04fc65e29899d206c7fb389346ea8ea906bae9 (diff) | |
Mini-restructuration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index cef0d1dea..97a6c4ca9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -377,8 +377,8 @@ let prec_assoc = function let precedence_of_entry_type from = function | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n - | ETConstr (NumLevel n,BorderProd (left,Some a)) -> - n, let (lp,rp) = prec_assoc a in if left then lp else rp + | ETConstr (NumLevel n,BorderProd (b,Some a)) -> + n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp | ETConstr (NumLevel n,InternalProd) -> n, Prec n | ETConstr (NextLevel,_) -> from, L | ETOther ("constr","annot") -> 10, Prec 10 @@ -825,9 +825,9 @@ let compute_syntax_data (df,modifiers) = let innerlevel = NumLevel 200 in let typs = find_symbols - (NumLevel n,BorderProd(true,assoc)) + (NumLevel n,BorderProd(Left,assoc)) (innerlevel,InternalProd) - (NumLevel n,BorderProd(false,assoc)) + (NumLevel n,BorderProd(Right,assoc)) symbols in (* To globalize... *) let typs = List.map (set_entry_type etyps) typs in |