diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /tactics/hipattern.mli | |
| parent | 25dde2366a4db47e5da13b2bbe4d03a31235706f (diff) | |
Added "etransitivity".
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hipattern.mli')
| -rw-r--r-- | tactics/hipattern.mli | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 3418dd208..5be8b2026 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -16,6 +16,7 @@ open Sign open Evd open Pattern open Proof_trees +open Coqlib (*i*) (*s Given a term with second-order variables in it, @@ -81,11 +82,9 @@ val is_unit_or_eq_type : testing_function (* type with only one constructor and no arguments, no indices *) val is_unit_type : testing_function -val match_with_equation : (constr * constr list) matching_function -val is_equation : testing_function - (* type with only one constructor, no arguments and at least one dependency *) val match_with_equality_type : (constr * constr list) matching_function +val is_equality_type : testing_function val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function @@ -110,14 +109,23 @@ val is_nodep_ind : testing_function val match_with_sigma_type : (constr * constr list) matching_function val is_sigma_type : testing_function -(***** Destructing patterns bound to some theory *) +(* Recongnize inductive relation defined by reflexivity *) -open Coqlib +type equation_kind = + | MonomorphicLeibnizEq of constr * constr + | PolymorphicLeibnizEq of constr * constr * constr + | HeterogenousEq of constr * constr * constr * constr + +exception NoEquationFound + +val match_with_equation: + constr -> coq_eq_data option * constr * equation_kind + +(***** Destructing patterns bound to some theory *) (* Match terms [(eq A t u)] or [(identity A t u)] *) (* Returns associated lemmas and [A,t,u] *) -val find_eq_data_decompose : constr -> - coq_leibniz_eq_data * (constr * constr * constr) +val find_eq_data_decompose : constr -> coq_eq_data * equation_kind (* Match a term of the form [(existT A P t p)] *) (* Returns associated lemmas and [A,P,t,p] *) |