From ae9b8392410ceb09e30c90c8863fc24a4c67b376 Mon Sep 17 00:00:00 2001
From: glondu
Date: Sat, 25 Dec 2010 23:07:21 +0000
Subject: ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED

Rationale: the expansion ignores the TYPED clause when
{RAW,GLOB}_TYPED are given. Indeed, in this case, the final type is a
consequence of either "INTERPRETED BY" (if given), or the default one
based on GLOB_TYPED.

This avoids the pitfall of the "raw" argument extension, where the
TYPED clause was unused and totally misleading.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13760 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/g_indfun.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index fb053c032f..39f4cf07f3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -56,7 +56,6 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 
 
 ARGUMENT EXTEND fun_ind_using
-  TYPED AS constr_with_bindings_opt
   PRINTED BY pr_fun_ind_using_typed
   RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
-- 
cgit v1.2.3