diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-17 17:31:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:39 +0200 |
| commit | 602544c70684794e34030757ff986eaa5b519069 (patch) | |
| tree | a22ea0ee9b68025b5ee974b7c471da2b5ee46fc4 /tactics/hipattern.ml4 | |
| parent | ca36da7eaa33f07c0bc9163fa10b017478c2ee0f (diff) | |
A few more comments in tactics.mli and hippatern.ml.
Diffstat (limited to 'tactics/hipattern.ml4')
| -rw-r--r-- | tactics/hipattern.ml4 | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index dc78229f6..e171c2147 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -274,6 +274,11 @@ let match_with_equation t = else raise NoEquationFound | _ -> raise NoEquationFound +(* Note: An "equality type" is any type with a single argument-free + constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also + True/unit which is the degenerate equality type (isomorphic to ()=()); + in particular, True/unit are provable by "reflexivity" *) + let is_inductive_equality ind = let (mib,mip) = Global.lookup_inductive ind in let nconstr = Array.length mip.mind_consnames in @@ -287,6 +292,8 @@ let match_with_equality_type t = let is_equality_type t = op2bool (match_with_equality_type t) +(* Arrows/Implication/Negation *) + let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ] let match_arrow_pattern t = @@ -296,6 +303,13 @@ let match_arrow_pattern t = assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) | _ -> anomaly (Pp.str "Incorrect pattern matching") +let match_with_imp_term c= + match kind_of_term c with + | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) + | _ -> None + +let is_imp_term c = op2bool (match_with_imp_term c) + let match_with_nottype t = try let (arg,mind) = match_arrow_pattern t in @@ -304,6 +318,8 @@ let match_with_nottype t = let is_nottype t = op2bool (match_with_nottype t) +(* Forall *) + let match_with_forall_term c= match kind_of_term c with | Prod (nam,a,b) -> Some (nam,a,b) @@ -311,13 +327,6 @@ let match_with_forall_term c= let is_forall_term c = op2bool (match_with_forall_term c) -let match_with_imp_term c= - match kind_of_term c with - | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) - | _ -> None - -let is_imp_term c = op2bool (match_with_imp_term c) - let match_with_nodep_ind t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with |