aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/argextend.ml4
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-07-05 19:22:49 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-07-05 19:22:49 +0000
commit931bd73212b0095d8c50e0355ee66faa32bf8db6 (patch)
treefbff2b6bf249899f4cdcd6d2a821d5259c177d7b /grammar/argextend.ml4
parenta778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 (diff)
Removing SortArgType.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar/argextend.ml4')
-rw-r--r--grammar/argextend.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index d8f615a98..128b13bda 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -36,7 +36,6 @@ let rec make_wit loc = function
| RefArgType -> <:expr< Constrarg.wit_ref >>
| QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
| GenArgType -> <:expr< Constrarg.wit_genarg >>
- | SortArgType -> <:expr< Constrarg.wit_sort >>
| ConstrArgType -> <:expr< Constrarg.wit_constr >>
| ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
| RedExprArgType -> <:expr< Constrarg.wit_red_expr >>