package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GentacticSource

Generic tactic expressions. Internally implemented using Genarg.

Sourcetype raw_generic_tactic
Sourcetype glob_generic_tactic

The genarg must have registrations for all the following APIs.

The genarg must have registrations for all the following APIs except those operating at the "raw" level.

Sourceval intern : ?strict:bool -> Environ.env -> ?ltacvars:Names.Id.Set.t -> raw_generic_tactic -> glob_generic_tactic

strict is default true

For serlib