fix virtual positions for symbols and rules generated by inductive

[fblanqui]

Remark on sym_pos vs sym_decl_pos:

• For a user-defined symbol s, s.sym_pos refers to the position of the symbol name in the user source file while s.sym_decl_pos refers to the position of the whole symbol command. These two positions are actual positions in the user source file.
• For a string literal symbol s, both s.sym_pos and s.sym_decl_pos refer to the position of the first occurrence of that string in the required user source files. They are actual positions.
• For an axiom symbol s generated while declaring a symbol t in a user source file, s.sym_pos refers to t.sym_pos (this would be better to take t.sym_decl_pos) and s.sym_decl_pos is a virtual position that generally occurs before t.sym_pos and t.sym_decl_pos, although this is not guaranteed (this should be fixed).
• For a generated symbol s that is an inductive type, constructor or recursor, s.sym_pos refers to the position of the inductive command in the user source file, and s.sym_decl_pos is a virtual position occurring after s.sym_pos.

Virtual positions are used to order symbol and rule declarations in commands exporting signatures. This is a hack that should be changed.

Modifications:

• fix Pos.pos_end by setting start_offset properly
• remove Pos.before (unused)
• unfold Pos.after to Pos.shift 1 to easily localize all the uses of shift
• Tactic.p_term_of_string_term: fix initial buffer position using pos_of_string
• rename Lcr.shift into Lcr.reindex to avoid confusion with Pos.shift

Remaining problems:

• in axioms, use sym_decl_pos instead of sym_pos ?
• axiom positions may not be before sym_decl_pos
• Indexing.index_sym needs to use sym_decl_pos, which is invalid for generated symbols
• Fix dk export on indind and file.with.dot #820

TODO in a future PR: add a new integer field sym_offset to order declarations wrt sym_decl_pos+sym_offset

[fblanqui]

@sacerdot Is it all right in index_sym to use sym_pos instead of sym_decl ?

[sacerdot]

No, I don't think so. The position corresponds to what it is fetched back and printed in the list of results. We want to print the whole symbol declaration, not just the name.

[fblanqui]

I see. I'm going to revert the change on indexing.ml. But, then, we need to use something better than virtual positions to order declarations.