package rocq-runtime

  1. Overview
  2. Docs

Source file coqlib.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(** Deprecated alias for Coqlib *)

include Rocqlib

open Names

type coq_sigma_data = rocq_sigma_data = {
  proj1 : GlobRef.t;
  proj2 : GlobRef.t;
  elim  : GlobRef.t;
  intro : GlobRef.t;
  typ   : GlobRef.t }

type coq_eq_data = rocq_eq_data = {
  eq   : GlobRef.t;
  ind  : GlobRef.t;
  refl : GlobRef.t;
  sym  : GlobRef.t;
  trans: GlobRef.t;
  congr: GlobRef.t }

let build_coq_eq_data = build_rocq_eq_data
let build_coq_identity_data = build_rocq_identity_data
let build_coq_jmeq_data = build_rocq_jmeq_data