Skip to content

Adapt map_term_with_context for 9.1 guard condition#1234

Open
BasileGros wants to merge 3 commits intoMetaRocq:9.1from
BasileGros:9.1
Open

Adapt map_term_with_context for 9.1 guard condition#1234
BasileGros wants to merge 3 commits intoMetaRocq:9.1from
BasileGros:9.1

Conversation

@BasileGros
Copy link

Adds back a change lost in the confusion of the transfer from 9.0 to 9.1 of an adaptation of map_term_with_context to work with the 9.1 guard condition.

Previous version does not allow to define in 9.1 the following MWE function:

Fixpoint convert_var_to_rel (glob : global_env)  (lctx : context) (t:term) {struct t} :=
  match t with
  |tVar _ => tRel (S (length lctx))
  |_ => map_term_with_context glob (convert_var_to_rel glob) lctx t
  end.

Basile added 3 commits November 17, 2025 17:55
# Conflicts:
#	template-rocq/theories/AstUtils.v
#	template-rocq/theories/Checker.v
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant