The Coq mailing list

["Eric Jaeger \(SGDN\)" <eric.jaeger AT sgdn.pm.gouv.fr>]

Hi,

After some time working with Coq, I've chosen for one of my projects (in 
which I don't care about impredicativity or proof irrelevance, but have 
difficulties to "eliminate" Prop hypothesis with a Set goal) to work without 
using the Prop sort, but Set instead... It's of course fine for my 
definitions, etc. and I was happy to discover that tactics such as rewrite 
can use identity as well as equality. However, I still have difficulties to 
get rid of Prop - in particular as far as equality is concerned.

As an example, if for "S:Set" I define "Inductive 
ind_id:S->S->Set:=ii_intro:forall (a:S), ind_id a a", then the inversion 
tactic applied to an hypothesis "ind_id a b" will return "a=b", while I 
would prefer "identity a b".

Is there a solution to work with Coq without using Prop at all ? Or, at 
least, to have Coq generate indentity results instead of equality results ?

Thanks for any help, Eric Jaeger