diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 09:26:08 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 09:26:08 +0000 |
| commit | 9330bf650ca602884c5c4c69c2fb3e94ee32838b (patch) | |
| tree | 5947d599c9c408680236995b11a47ab93703b701 /grammar | |
| parent | 02077f5b5e132e135be778c201e74a5eb87b97ae (diff) | |
Implemented a full-fledged equality on [constr_expr]. By the way,
some cleaning of the interface and moving of code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 757df76a6..50eac6e76 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -34,7 +34,10 @@ Argextend Tacextend Vernacextend +Nameops Redops +Miscops +Glob_ops Constrexpr_ops Locusops G_prim |