~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to plugins/subtac/subtac_utils.ml

• browse files at revision 6
• compare with another revision
• download diff
• download tarball
• view history from revision 6

Show diffs side-by-side

added

removed

plugins/subtac/subtac_utils.ml

23

23

let init_constant dir s () = gen_constant contrib_name dir s

24

24

let init_reference dir s () = gen_reference contrib_name dir s

25

25

 

 

26

let safe_init_constant md name () =

 

27

  check_required_library ("Coq"::md);

 

28

  init_constant md name ()

 

29

 

26

30

let fixsub = init_constant fixsub_module "Fix_sub"

27

31

let ex_pi1 = init_constant utils_module "ex_pi1"

28

32

let ex_pi2 = init_constant utils_module "ex_pi2"

74

78

let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"

75

79

 

76

80

let jmeq_ind =

77

 

  init_constant ["Logic";"JMeq"] "JMeq"

 

81

  safe_init_constant ["Logic";"JMeq"] "JMeq"

78

82

 

79

83

let jmeq_rec =

80

84

  init_constant ["Logic";"JMeq"] "JMeq_rec"

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1