diff options
| author | herbelin | 2009-01-19 11:05:02 +0000 |
|---|---|---|
| committer | herbelin | 2009-01-19 11:05:02 +0000 |
| commit | 8a2c029b0ae88888efe707c00f1a288e5c17cfb3 (patch) | |
| tree | 6beeccea6ceb18de008abeb910694827d952344d /toplevel | |
| parent | 85237f65161cb9cd10119197c65c84f65f0262ee (diff) | |
- Structuring Numbers and fixing Setoid in stdlib's doc.
- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 234dd04c42..75a6a8e755 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -743,7 +743,7 @@ let set_entry_type etyps (x,typ) = | ETConstr (n,()), (_,BorderProd (left,_)) -> ETConstr (n,BorderProd (left,None)) | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd) - | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t + | (ETPattern | ETName | ETBigint | ETOther _ | ETReference as t), _ -> t | (ETConstrList _, _) -> assert false with Not_found -> ETConstr typ in (x,typ) @@ -764,7 +764,7 @@ let find_precedence lev etyps symbols = (try match List.assoc x etyps with | ETConstr _ -> error "The level of the leftmost non-terminal cannot be changed." - | ETIdent | ETBigint | ETReference -> + | ETName | ETBigint | ETReference -> if lev = None then Flags.if_verbose msgnl (str "Setting notation at level 0.") else |