package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Tactic related witnesses, could also live in tactics/ if other users

  • deprecated Use wit_simple_intropattern

Generic arguments based on Ltac.

wit_ltac is subtly different from wit_tactic: they only change for their toplevel interpretation. The one of wit_ltac forces the tactic and discards the result.

OCaml

Innovation. Community. Security.