diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.mli')
| -rw-r--r-- | contrib/subtac/subtac_utils.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index a87bbfbeda..5a5dd4274b 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -100,6 +100,12 @@ val mkProj1 : constr -> constr -> constr -> constr val mkProj1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr +val mk_eq : types -> constr -> constr -> types +val mk_eq_refl : types -> constr -> constr +val mk_JMeq : types -> constr-> types -> constr -> types +val mk_JMeq_refl : types -> constr -> constr +val mk_conj : types list -> types +val mk_not : types -> types val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> |