diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /contrib/subtac/subtac_cases.ml | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 *) |