From 128a297614d1e0fb32e2bbd465d181c5d5b1562c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 Aug 2014 14:27:23 +0200 Subject: A tentative uniform naming policy in module Inductiveops. - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls --- checker/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/indtypes.ml') diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 14710c10b..49d78a7a6 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -160,7 +160,7 @@ let typecheck_arity env params inds = if ind.mind_nrealargs <> nrealargs then failwith "bad number of real inductive arguments"; let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in - if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then + if ind.mind_nrealdecls <> nrealargs_ctxt then failwith "bad length of real inductive arguments signature"; (* We do not need to generate the universe of full_arity; if later, after the validation of the inductive definition, -- cgit v1.2.3