The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Would things get naturally simpler using Set rather than Type in that case?

My understanding is that Set is much simpler than Type, so I stick to
Set for data structures as much as possible (though it is not trendy).
For instance, nat: Set.
Having list : Type -> Type is reasonable in order to have lists 
of anything once for all, including lists of proofs, lists of Props, lists 
of types, etc.

For the case of Sylvain, is Type really needed?

Jean-Francois

On Thu, Oct 06, 2016 at 09:22:17AM +0200, Guillaume Melquiond wrote:
> On 06/10/2016 09:13, Sylvain Boulmé wrote:
> 
> > But, when using this tactic inside a Coq module "TestTactic", I get the
> > following error message:
> > 
> > Error: Illegal application:
> > The term "Syntax.Var" of type
> >  "forall var : Type, var -> Syntax.expr var"
> > cannot be applied to the terms
> >  "v" : "Type"
> >  "r4" : "v"
> > The 1st term has type "Type@{TestTactic.1}"
> > which should be coercible to "Type@{Syntax.1}".
> > 
> > 
> > How to correct my code above ?
> 
> As far as I know, you are supposed to call Typing.type_of on your newly
> created term. That will return a new evarmap that should pass to
> tclEVARS rather than the old one (which does not contain enough universe
> constraints for checking that your new term is well-typed).
> 
> Unfortunately, it means type-checking your term twice, which you
> precisely wanted to avoid since you are calling exact_no_check. Another
> solution is thus not too call Typing.type_of on your new term, but on a
> smaller simpler dummy term. If your dummy term (whatever its type)
> happens to produce the exact same universe constraints as your new term,
> then you are good to go and you can use the produced evarmap instead.
> 
> Best regards,
> 
> Guillaume