diff options
Diffstat (limited to 'contrib/subtac/subtac_cases.ml')
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index c7182bd2..04bf54d3 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *) +(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Cases open Util @@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs sign (lift tomatchs_len t) in - let arity = - it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs) + let neqs, arity = + let ctx = context_of_arsign eqs in + let neqs = List.length ctx in + neqs, it_mkProd_or_LetIn (lift neqs arity) ctx in let lets, matx = (* Type the rhs under the assumption of equations *) |