aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--contrib/funind/invfun.ml4
-rw-r--r--doc/refman/RefMan-tac.tex161
-rw-r--r--pretyping/clenv.ml15
-rw-r--r--pretyping/evd.ml18
-rw-r--r--pretyping/termops.ml5
-rw-r--r--pretyping/termops.mli3
-rw-r--r--proofs/clenvtac.ml3
-rw-r--r--proofs/clenvtac.mli1
-rw-r--r--tactics/eqdecide.ml44
-rw-r--r--tactics/equality.ml148
-rw-r--r--tactics/equality.mli24
-rw-r--r--tactics/extratactics.ml484
-rw-r--r--tactics/extratactics.mli5
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tactics.ml33
-rw-r--r--tactics/tactics.mli7
-rw-r--r--test-suite/success/Discriminate.v23
-rw-r--r--test-suite/success/Injection.v27
-rw-r--r--toplevel/auto_ind_decl.ml9
22 files changed, 409 insertions, 176 deletions
diff --git a/CHANGES b/CHANGES
index 4304fce18..675db3f18 100644
--- a/CHANGES
+++ b/CHANGES
@@ -202,6 +202,9 @@ Tactics
- Slight improvement of the hnf and simpl tactics when applied on
expressions with explicit occurrences of match or fix.
- New tactics "eapply in", "erewrite", "erewrite in".
+- New tactics "ediscriminate", "einjection", "esimplify_eq".
+- Tactics "discriminate", "injection", "simplify_eq" now support any
+ term as argument. Clause "with" is also supported.
- Unfoldable references can be given by notation's string rather than by name
in unfold.
- The "with" arguments are now typed using informations from the current goal:
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 0160c290f..63d44916b 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -573,9 +573,9 @@ let rec reflexivity_with_destruct_cases g =
match kind_of_term (pf_type_of g (mkVar id)) with
| App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
- then Equality.discr id g
+ then Equality.discrHyp id g
else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite] g
+ then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f71d66319..8539136a0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -993,7 +993,7 @@ The proof of {\tt False} is searched in the hypothesis named \ident.
\tacindex{contradict}
This tactic allows to manipulate negated hypothesis and goals. The
-name \ident\ should correspond to an hypothesis. With
+name \ident\ should correspond to a hypothesis. With
{\tt contradict H}, the current goal and context is transformed in
the following way:
\begin{itemize}
@@ -2395,17 +2395,20 @@ of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals
of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic
\texttt{decide equality}.
-\subsection{\tt discriminate {\ident}
+\subsection{\tt discriminate {\term}
\label{discriminate}
-\tacindex{discriminate}}
+\tacindex{discriminate}
+\tacindex{ediscriminate}}
-This tactic proves any goal from an absurd hypothesis stating that two
+This tactic proves any goal from an assumption stating that two
structurally different terms of an inductive set are equal. For
-example, from the hypothesis {\tt (S (S O))=(S O)} we can derive by
-absurdity any proposition. Let {\ident} be a hypothesis of type
-{\tt{\term$_1$} = {\term$_2$}} in the local context, {\term$_1$} and
+example, from {\tt (S (S O))=(S O)} we can derive by absurdity any
+proposition.
+
+The argument {\term} is assumed to be a proof of a statement
+of conclusion {\tt{\term$_1$} = {\term$_2$}} with {\term$_1$} and
{\term$_2$} being elements of an inductive set. To build the proof,
-the tactic traverses the normal forms\footnote{Recall: opaque
+the tactic traverses the normal forms\footnote{Reminder: opaque
constants will not be expanded by $\delta$ reductions} of
{\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u}
and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and
@@ -2414,26 +2417,39 @@ positions and whose head symbols are two different constructors. If
such a couple of subterms exists, then the proof of the current goal
is completed, otherwise the tactic fails.
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem The syntax {\tt discriminate {\ident}} can be used to refer to a
+hypothesis quantified in the goal. In this case, the quantified
+hypothesis whose name is {\ident} is first introduced in the local
+context using \texttt{intros until \ident}.
\begin{ErrMsgs}
-\item {\ident} \errindex{Not a discriminable equality} \\
- occurs when the type of the specified hypothesis is not an equation.
+\item \errindex{No primitive equality found}
+\item \errindex{Not a discriminable equality}
\end{ErrMsgs}
\begin{Variants}
-\item \texttt{discriminate} \num\\
- This does the same thing as \texttt{intros until \num} then
-\texttt{discriminate \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-\item {\tt discriminate}\\
- It applies to a goal of the form {\tt
- \verb=~={\term$_1$}={\term$_2$}} and it is equivalent to:
- {\tt unfold not; intro {\ident}}; {\tt discriminate
- {\ident}}.
+\item \texttt{discriminate} \num
+
+ This does the same thing as \texttt{intros until \num} followed by
+ \texttt{discriminate \ident} where {\ident} is the identifier for
+ the last introduced hypothesis.
+
+\item \texttt{discriminate} {\term} {\tt with} {\bindinglist}
+
+ This does the same thing as \texttt{discriminate {\term}} but using
+the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{ediscriminate} \num\\
+ \texttt{ediscriminate} {\term} \zeroone{{\tt with} {\bindinglist}}
+
+ This works the same as {\tt discriminate} but if the type of {\term},
+ or the type of the hypothesis referred to by {\num}, has uninstantiated
+ parameters, these parameters are left as existential variables.
+
+\item \texttt{discriminate}
+
+ This looks for a quantified or not quantified hypothesis {\ident} on
+ which {\tt discriminate {\ident}} is applicable.
\begin{ErrMsgs}
\item \errindex{No discriminable equalities} \\
@@ -2441,9 +2457,10 @@ introduced hypothesis.
\end{ErrMsgs}
\end{Variants}
-\subsection{\tt injection {\ident}
+\subsection{\tt injection {\term}
\label{injection}
-\tacindex{injection}}
+\tacindex{injection}
+\tacindex{einjection}}
The {\tt injection} tactic is based on the fact that constructors of
inductive sets are injections. That means that if $c$ is a constructor
@@ -2451,10 +2468,11 @@ of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
too.
-If {\ident} is an hypothesis of type {\tt {\term$_1$} = {\term$_2$}},
-then {\tt injection} behaves as applying injection as deep as possible to
+If {\term} is a proof of a statement of conclusion
+ {\tt {\term$_1$} = {\term$_2$}},
+then {\tt injection} applies injectivity as deep as possible to
derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
-placed in the same positions. For example, from the hypothesis {\tt (S
+placed in the same positions. For example, from {\tt (S
(S n))=(S (S (S m))} we may derive {\tt n=(S m)}. To use this
tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
set and they should be neither explicitly equal, nor structurally
@@ -2462,7 +2480,7 @@ different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
their respective normal forms, then:
\begin{itemize}
\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
-\item there must not exist any couple of subterms {\tt u} and {\tt w},
+\item there must not exist any pair of subterms {\tt u} and {\tt w},
{\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
placed in the same positions and having different constructors as
head symbols.
@@ -2501,59 +2519,70 @@ the projection on the second one, and so {\tt injection} will work fine.
To define such an equality, you have to use the {\tt Scheme} command
(see \ref{Scheme}).
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt injection {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
\begin{ErrMsgs}
-\item {\ident} \errindex{is not a projectable equality}
- occurs when the type of
- the hypothesis $id$ does not verify the preconditions.
-\item \errindex{Not an equation} occurs when the type of the
- hypothesis $id$ is not an equation.
+\item \errindex{Not a projectable equality but a discriminable one}
+\item \errindex{Nothing to do, it is an equality between convertible terms}
+\item \errindex{Not a primitive equality}
\end{ErrMsgs}
\begin{Variants}
\item \texttt{injection} \num{}
- This does the same thing as \texttt{intros until \num} then
+ This does the same thing as \texttt{intros until \num} followed by
\texttt{injection \ident} where {\ident} is the identifier for the last
introduced hypothesis.
-\item{\tt injection}\tacindex{injection}
+\item \texttt{injection} \term{} {\tt with} {\bindinglist}
+
+ This does the same as \texttt{injection {\term}} but using
+ the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{einjection} \num\\
+ \texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+ This works the same as {\tt injection} but if the type of {\term},
+ or the type of the hypothesis referred to by {\num}, has uninstantiated
+ parameters, these parameters are left as existential variables.
+
+\item{\tt injection}
If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
- the tactic computes the head normal form of the goal and then
- behaves as the sequence: {\tt unfold not; intro {\ident}; injection
- {\ident}}.
+ this behaves as {\tt intro {\ident}; injection {\ident}}.
\ErrMsg \errindex{goal does not satisfy the expected preconditions}
-\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\
+\item \texttt{injection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
\texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
\texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
+\texttt{einjection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
\tacindex{injection \ldots{} as}
-These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}.
+These variants apply \texttt{intros} \nelist{\intropattern}{} after
+the call to \texttt{injection} or \texttt{einjection}.
\end{Variants}
-\subsection{\tt simplify\_eq {\ident}
+\subsection{\tt simplify\_eq {\term}
\tacindex{simplify\_eq}
+\tacindex{esimplify\_eq}
\label{simplify-eq}}
-Let {\ident} be the name of an hypothesis of type {\tt
- {\term$_1$}={\term$_2$}} in the local context. If {\term$_1$} and
+Let {\term} be the proof of a statement of conclusion {\tt
+ {\term$_1$}={\term$_2$}}. If {\term$_1$} and
{\term$_2$} are structurally different (in the sense described for the
tactic {\tt discriminate}), then the tactic {\tt simplify\_eq} behaves as {\tt
- discriminate {\ident}} otherwise it behaves as {\tt injection
- {\ident}}.
+ discriminate {\term}}, otherwise it behaves as {\tt injection
+ {\term}}.
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt simplify\_eq {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
\begin{Variants}
\item \texttt{simplify\_eq} \num
@@ -2561,9 +2590,23 @@ latter is first introduced in the local context using
This does the same thing as \texttt{intros until \num} then
\texttt{simplify\_eq \ident} where {\ident} is the identifier for the last
introduced hypothesis.
+
+\item \texttt{simplify\_eq} \term{} {\tt with} {\bindinglist}
+
+ This does the same as \texttt{simplify\_eq {\term}} but using
+ the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{esimplify\_eq} \num\\
+ \texttt{esimplify\_eq} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+ This works the same as {\tt simplify\_eq} but if the type of {\term},
+ or the type of the hypothesis referred to by {\num}, has uninstantiated
+ parameters, these parameters are left as existential variables.
+
\item{\tt simplify\_eq}
-If the current goal has form $\verb=~=t_1=t_2$, then this tactic does
-\texttt{hnf; intro {\ident}; simplify\_eq {\ident}}.
+
+If the current goal has form $t_1\verb=<>=t_2$, it behaves as
+\texttt{intro {\ident}; simplify\_eq {\ident}}.
\end{Variants}
\subsection{\tt dependent rewrite -> {\ident}
@@ -2599,8 +2642,8 @@ constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
conditions that should hold for the instance $(I~\vec{t})$ to be
proved by $c_i$.
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
+\Rem If {\ident} does not denote a hypothesis in the local context
+but refers to a hypothesis quantified in the goal, then the
latter is first introduced in the local context using
\texttt{intros until \ident}.
@@ -3242,7 +3285,7 @@ equalities with uninterpreted symbols. It also include the constructor theory
(see \ref{injection} and \ref{discriminate}).
If the goal is a non-quantified equality, {\tt congruence} tries to
prove it with non-quantified equalities in the context. Otherwise it
-tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
+tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.
{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for {\tt congruence} to match against it.
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 074dd0901..c91580044 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -222,13 +222,24 @@ let dependent_metas clenv mvs conclmetas =
Metaset.union deps (clenv_metavars clenv.evd mv))
mvs conclmetas
+let duplicated_metas c =
+ let rec collrec (one,more as acc) c =
+ match kind_of_term c with
+ | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
+ | _ -> fold_constr collrec acc c
+ in
+ snd (collrec ([],[]) c)
+
let clenv_dependent hyps_only clenv =
let mvs = undefined_metas clenv.evd in
let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
let deps = dependent_metas clenv mvs ctyp_mvs in
+ let nonlinear = duplicated_metas (clenv_value clenv) in
+ (* Make the assumption that duplicated metas have internal dependencies *)
List.filter
- (fun mv -> Metaset.mem mv deps &&
- not (hyps_only && Metaset.mem mv ctyp_mvs))
+ (fun mv -> (Metaset.mem mv deps &&
+ not (hyps_only && Metaset.mem mv ctyp_mvs))
+ or List.mem mv nonlinear)
mvs
let clenv_missing ce = clenv_dependent true ce
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 660547b5c..166114ab6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -643,6 +643,20 @@ type unsolvability_explanation = SeveralInstancesFound of int
(**********************************************************)
(* Pretty-printing *)
+let pr_instance_status (sc,typ) =
+ begin match sc with
+ | IsSubType -> str " [or a subtype of it]"
+ | IsSuperType -> str " [or a supertype of it]"
+ | ConvUpToEta 0 -> mt ()
+ | UserGiven -> mt ()
+ | ConvUpToEta n -> str" [or an eta-expansion up to " ++ int n ++ str" of it]"
+ end ++
+ begin match typ with
+ | CoerceToType -> str " [up to coercion]"
+ | TypeNotProcessed -> mt ()
+ | TypeProcessed -> str " [type is checked]"
+ end
+
let pr_meta_map mmap =
let pr_name = function
Name id -> str"[" ++ pr_id id ++ str"]"
@@ -652,10 +666,10 @@ let pr_meta_map mmap =
hov 0
(pr_meta mv ++ pr_name na ++ str " : " ++
print_constr b.rebus ++ fnl ())
- | (mv,Clval(na,(b,_),_)) ->
+ | (mv,Clval(na,(b,s),_)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " := " ++
- print_constr b.rebus ++ fnl ())
+ print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ())
in
prlist pr_meta_binding (metamap_to_list mmap)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 73c03097a..4246f0daa 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -275,6 +275,11 @@ let rec strip_head_cast c = match kind_of_term c with
| Cast (c,_,_) -> strip_head_cast c
| _ -> c
+(* Get the last arg of an application *)
+let last_arg c = match kind_of_term c with
+ | App (f,cl) -> array_last cl
+ | _ -> anomaly "last_arg"
+
(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
subterms of [c]; it carries an extra data [l] (typically a name
list) which is processed by [g na] (which typically cons [na] to
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f80deab10..539951d5c 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -185,6 +185,9 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types
val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+(* Get the last arg of a constr intended to be nn application *)
+val last_arg : constr -> constr
+
(* name contexts *)
type names_context = name list
val add_name : name -> names_context -> names_context
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 22dcca289..624b671d3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -60,6 +60,9 @@ let clenv_cast_meta clenv =
in
crec
+let clenv_value_cast_meta clenv =
+ clenv_cast_meta clenv (clenv_value clenv)
+
let clenv_pose_dependent_evars with_evars clenv =
let dep_mvs = clenv_dependent false clenv in
if dep_mvs <> [] & not with_evars then
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 0cf0a5545..4dd59fcf6 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -27,6 +27,7 @@ val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify
val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_value_cast_meta : clausenv -> constr
(* Compatibility, use res_pf ?with_evars:true instead *)
val e_res_pf : clausenv -> tactic
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 8aef9c50b..61100f0a5 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -75,7 +75,7 @@ let mkBranches c1 c2 =
let solveNoteqBranch side =
tclTHEN (choose_noteq side)
(tclTHEN (intro_force true)
- (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
+ (onLastHyp (fun id -> Extratactics.h_discrHyp id)))
let h_solveNoteqBranch side =
Refiner.abstract_extended_tactic "solveNoteqBranch" []
@@ -115,7 +115,7 @@ let diseqCase eqonleft =
(tclTHEN red_in_concl
(tclTHEN (intro_using absurd)
(tclTHEN (h_simplest_apply (mkVar diseq))
- (tclTHEN (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
+ (tclTHEN (Extratactics.h_injHyp absurd)
(full_trivial [])))))))
let solveArg eqonleft op a1 a2 tac g =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f907b1fd7..3bfc719e2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,6 +40,9 @@ open Vernacexpr
open Setoid_replace
open Declarations
open Indrec
+open Printer
+open Clenv
+open Clenvtac
(* Rewriting tactics *)
@@ -550,66 +553,84 @@ exception NotDiscriminable
let eq_baseid = id_of_string "e"
-let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort =
+let apply_on_clause (f,t) clause =
+ let sigma = Evd.evars_of clause.evd in
+ let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
+ let argmv =
+ (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
+ | Meta mv -> mv
+ | _ -> errorlabstrm "" (str "Ill-formed clause applicator")) in
+ clenv_fchain argmv f_clause clause
+
+let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (e,None,t) env in
+ let eqn = mkApp(lbeq.eq,[|t;t1;t2|]) in
let discriminator =
build_discriminator sigma e_env dirn (mkVar e) sort cpath in
let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
- tclCOMPLETE
- ((tclTHENS (cut_intro absurd_term)
- [onLastHyp gen_absurdity;
- refine (mkApp (pf,[|mkVar id|]))]))
+ let pf_ty = mkArrow eqn absurd_term in
+ let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
+ tclTHENS (cut_intro absurd_term)
+ [onLastHyp gen_absurdity; res_pf absurd_clause]
-let discrEq (lbeq,(t,t1,t2) as u) id gls =
- let sigma = project gls in
+let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
+ let sigma = Evd.evars_of eq_clause.evd in
let env = pf_env gls in
match find_positions env sigma t1 t2 with
| Inr _ ->
- errorlabstrm "discr" (str" Not a discriminable equality")
+ errorlabstrm "discr" (str"Not a discriminable equality")
| Inl (cpath, (_,dirn), _) ->
let sort = pf_apply get_type_of gls (pf_concl gls) in
- discr_positions env sigma u id cpath dirn sort gls
-
-let onEquality tac id gls =
- let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+ discr_positions env sigma u eq_clause cpath dirn sort gls
+
+let onEquality with_evars tac (c,lbindc) gls =
+ let t = pf_type_of gls c in
+ let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in
+ let eq_clause = make_clenv_binding gls (c,t') lbindc in
+ let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
+ let eqn = clenv_type eq_clause' in
let eq =
try find_eq_data_decompose eqn
with PatternMatchingFailure ->
- errorlabstrm "" (pr_id id ++ str": not a primitive equality")
- in tac eq id gls
+ errorlabstrm "" (str"No primitive equality found") in
+ tclTHEN
+ (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd))
+ (tac eq eq_clause') gls
-let onNegatedEquality tac gls =
+let onNegatedEquality with_evars tac gls =
let ccl = pf_concl gls in
- let eq =
- try match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
- | Prod (_,t,u) when is_empty_type u ->
- find_eq_data_decompose (pf_whd_betadeltaiota gls t)
- | _ -> raise PatternMatchingFailure
- with PatternMatchingFailure ->
+ match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
+ | Prod (_,t,u) when is_empty_type u ->
+ tclTHEN introf
+ (onLastHyp (fun id ->
+ onEquality with_evars tac (mkVar id,NoBindings))) gls
+ | _ ->
errorlabstrm "" (str "Not a negated primitive equality")
- in tclTHEN introf (onLastHyp (tac eq)) gls
-let discrSimpleClause = function
- | None -> onNegatedEquality discrEq
- | Some ((_,id),_) -> onEquality discrEq id
+let discrSimpleClause with_evars = function
+ | None -> onNegatedEquality with_evars discrEq
+ | Some ((_,id),_) -> onEquality with_evars discrEq (mkVar id,NoBindings)
-let discr = onEquality discrEq
+let discr with_evars = onEquality with_evars discrEq
-let discrClause = onClauses discrSimpleClause
+let discrClause with_evars = onClauses (discrSimpleClause with_evars)
-let discrEverywhere =
+let discrEverywhere with_evars =
tclORELSE
- (Tacticals.tryAllClauses discrSimpleClause)
+ (tclTHEN
+ (tclREPEAT introf)
+ (Tacticals.tryAllHyps
+ (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
(fun gls ->
errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
-let discr_tac = function
- | None -> discrEverywhere
- | Some id -> try_intros_until discr id
+let discr_tac with_evars = function
+ | None -> discrEverywhere with_evars
+ | Some c -> onInductionArg (discr with_evars) c
-let discrConcl gls = discrClause onConcl gls
-let discrHyp id gls = discrClause (onHyp id) gls
+let discrConcl gls = discrClause false onConcl gls
+let discrHyp id gls = discrClause false (onHyp id) gls
(* returns the sigma type (sigS, sigT) with the respective
constructor depending on the sort *)
@@ -828,7 +849,7 @@ let simplify_args env sigma t =
| eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
| _ -> t
-let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
+let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (e,None,t) env in
let injectors =
@@ -837,9 +858,12 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
(* arbitrarily take t1' as the injector default value *)
let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
let injfun = mkNamedLambda e t injbody in
- let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
- let ty = simplify_args env sigma (get_type_of env sigma pf) in
- (pf,ty))
+ let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
+ let pf_typ = get_type_of env sigma pf in
+ let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
+ let pf = clenv_value_cast_meta inj_clause in
+ let ty = simplify_args env sigma (clenv_type inj_clause) in
+ (pf,ty))
posns in
if injectors = [] then
errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
@@ -850,14 +874,13 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
exception Not_dep_pair
-let injEq ipats (eq,(t,t1,t2)) id gls =
- let sigma = project gls in
- let env = pf_env gls in
+let injEq ipats (eq,(t,t1,t2)) eq_clause =
+ let sigma = Evd.evars_of eq_clause.evd in
+ let env = eq_clause.env in
match find_positions env sigma t1 t2 with
| Inl _ ->
errorlabstrm "Inj"
- (str (string_of_id id) ++
- str" is not a projectable equality but a discriminable one")
+ (str"Not a projectable equality but a discriminable one")
| Inr [] ->
errorlabstrm "Equality.inj"
(str"Nothing to do, it is an equality between convertible terms")
@@ -895,45 +918,44 @@ let injEq ipats (eq,(t,t1,t2)) id gls =
[|ar1.(0);Ind_tables.find_eq_dec_proof ind;
ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
)) (Auto.trivial [] [])
- ] gls
+ ]
(* not a dep eq or no decidable type found *)
) else (raise Not_dep_pair)
- ) with _ -> (
- tclTHEN
- (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
+ ) with _ ->
+ tclTHEN
+ (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns)
(intros_pattern None ipats)
- gls
- )
-let inj ipats = onEquality (injEq ipats)
+let inj ipats with_evars = onEquality with_evars (injEq ipats)
-let injClause ipats = function
- | None -> onNegatedEquality (injEq ipats)
- | Some id -> try_intros_until (inj ipats) id
+let injClause ipats with_evars = function
+ | None -> onNegatedEquality with_evars (injEq ipats)
+ | Some c -> onInductionArg (inj ipats with_evars) c
-let injConcl gls = injClause [] None gls
-let injHyp id gls = injClause [] (Some id) gls
+let injConcl gls = injClause [] false None gls
+let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
-let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls =
+let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
let sort = pf_apply get_type_of gls (pf_concl gls) in
- let sigma = project gls in
+ let sigma = Evd.evars_of clause.evd in
let env = pf_env gls in
match find_positions env sigma t1 t2 with
| Inl (cpath, (_,dirn), _) ->
- discr_positions env sigma u id cpath dirn sort gls
+ discr_positions env sigma u clause cpath dirn sort gls
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
ntac 0 gls
| Inr posns ->
tclTHEN
- (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns))
+ (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause
+ (List.rev posns))
(ntac (List.length posns))
gls
-let dEqThen ntac = function
- | None -> onNegatedEquality (decompEqThen ntac)
- | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id
+let dEqThen with_evars ntac = function
+ | None -> onNegatedEquality with_evars (decompEqThen ntac)
+ | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
-let dEq = dEqThen (fun x -> tclIDTAC)
+let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
let rewrite_msg = function
| None -> str "passed term is not a primitive equality"
diff --git a/tactics/equality.mli b/tactics/equality.mli
index acbaca235..3c7f9c6b0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -67,18 +67,22 @@ val replace_in : identifier -> constr -> constr -> tactic
val replace_by : constr -> constr -> tactic -> tactic
val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
-val discr : identifier -> tactic
+val discr : evars_flag -> constr with_ebindings -> tactic
val discrConcl : tactic
-val discrClause : clause -> tactic
+val discrClause : evars_flag -> clause -> tactic
val discrHyp : identifier -> tactic
-val discrEverywhere : tactic
-val discr_tac : quantified_hypothesis option -> tactic
-val inj : intro_pattern_expr list -> identifier -> tactic
-val injClause : intro_pattern_expr list -> quantified_hypothesis option ->
- tactic
-
-val dEq : quantified_hypothesis option -> tactic
-val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic
+val discrEverywhere : evars_flag -> tactic
+val discr_tac : evars_flag ->
+ constr with_ebindings induction_arg option -> tactic
+val inj : intro_pattern_expr list -> evars_flag ->
+ constr with_ebindings -> tactic
+val injClause : intro_pattern_expr list -> evars_flag ->
+ constr with_ebindings induction_arg option -> tactic
+val injHyp : identifier -> tactic
+val injConcl : tactic
+
+val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic
+val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index dd716024d..5d374215d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -16,6 +16,8 @@ open Genarg
open Extraargs
open Mod_subst
open Names
+open Tacexpr
+open Rawterm
(* Equality *)
open Equality
@@ -41,25 +43,93 @@ TACTIC EXTEND replace_term
-> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
END
+let induction_arg_of_quantified_hyp = function
+ | AnonHyp n -> ElimOnAnonHyp n
+ | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id)
+
+(* Versions *_main must come first!! so that "1" is interpreted as a
+ ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
+ ElimOnIdent and not as "constr" *)
+
+TACTIC EXTEND simplify_eq_main
+| [ "simplify_eq" constr_with_bindings(c) ] ->
+ [ dEq false (Some (ElimOnConstr c)) ]
+END
TACTIC EXTEND simplify_eq
- [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
+ [ "simplify_eq" ] -> [ dEq false None ]
+| [ "simplify_eq" quantified_hypothesis(h) ] ->
+ [ dEq false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND esimplify_eq_main
+| [ "esimplify_eq" constr_with_bindings(c) ] ->
+ [ dEq true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND esimplify_eq
+| [ "esimplify_eq" ] -> [ dEq true None ]
+| [ "esimplify_eq" quantified_hypothesis(h) ] ->
+ [ dEq true (Some (induction_arg_of_quantified_hyp h)) ]
END
+TACTIC EXTEND discriminate_main
+| [ "discriminate" constr_with_bindings(c) ] ->
+ [ discr_tac false (Some (ElimOnConstr c)) ]
+END
TACTIC EXTEND discriminate
- [ "discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ]
+| [ "discriminate" ] -> [ discr_tac false None ]
+| [ "discriminate" quantified_hypothesis(h) ] ->
+ [ discr_tac false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND ediscriminate_main
+| [ "ediscriminate" constr_with_bindings(c) ] ->
+ [ discr_tac true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND ediscriminate
+| [ "ediscriminate" ] -> [ discr_tac true None ]
+| [ "ediscriminate" quantified_hypothesis(h) ] ->
+ [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ]
END
-let h_discrHyp id = h_discriminate (Some id)
+let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings)
+TACTIC EXTEND injection_main
+| [ "injection" constr_with_bindings(c) ] ->
+ [ injClause [] false (Some (ElimOnConstr c)) ]
+END
TACTIC EXTEND injection
- [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ]
+| [ "injection" ] -> [ injClause [] false None ]
+| [ "injection" quantified_hypothesis(h) ] ->
+ [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND einjection_main
+| [ "einjection" constr_with_bindings(c) ] ->
+ [ injClause [] true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND einjection
+| [ "einjection" ] -> [ injClause [] true None ]
+| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND injection_as_main
+| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+ [ injClause ipat false (Some (ElimOnConstr c)) ]
END
TACTIC EXTEND injection_as
- [ "injection" quantified_hypothesis_opt(h)
- "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ]
+| [ "injection" "as" simple_intropattern_list(ipat)] ->
+ [ injClause ipat false None ]
+| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+ [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ]
+END
+TACTIC EXTEND einjection_as_main
+| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+ [ injClause ipat true (Some (ElimOnConstr c)) ]
+END
+TACTIC EXTEND einjection_as
+| [ "einjection" "as" simple_intropattern_list(ipat)] ->
+ [ injClause ipat true None ]
+| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+ [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
END
-let h_injHyp id = h_injection (Some id)
+let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
TACTIC EXTEND conditional_rewrite
| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 341716c01..7a5314c36 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -9,10 +9,9 @@
(*i $Id$ i*)
open Proof_type
-open Rawterm
-val h_discrHyp : quantified_hypothesis -> tactic
-val h_injHyp : quantified_hypothesis -> tactic
+val h_discrHyp : Names.identifier -> tactic
+val h_injHyp : Names.identifier -> tactic
val refine_tac : Evd.open_constr -> tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a77a97906..a25fa285b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -331,7 +331,7 @@ let projectAndApply thin id eqname names depids gls =
substHypIfVariable
(* If no immediate variable in the equation, try to decompose it *)
(* and apply a trailer which again try to substitute *)
- (fun id -> dEqThen (deq_trailer id) (Some (NamedHyp id)))
+ (fun id -> dEqThen false (deq_trailer id) (Some (ElimOnIdent (dummy_loc,id))))
id
gls
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 876f13c33..897c8fd98 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1150,7 +1150,7 @@ let debugging_exception_step ist signal_anomaly e pp =
let error_ltac_variable loc id env v s =
user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
- str "which cannot be coerced to " ++ str s)
+ strbrk "which cannot be coerced to " ++ str s)
exception CannotCoerceTo of string
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 577ef0c6f..3d5fd753e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -325,10 +325,6 @@ let elimination_sort_of_hyp id gl =
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* c should be of type A1->.. An->B with B an inductive definition *)
-let last_arg c = match kind_of_term c with
- | App (f,cl) -> array_last cl
- | _ -> anomaly "last_arg"
-
let general_elim_then_using mk_elim
isrec allnames tac predicate (indbindings,elimbindings)
ind indclause gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25e920976..c8f92b60f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -469,6 +469,21 @@ let rec intros_rmove = function
move_to_rhyp destopt;
intros_rmove rest ]
+(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+ or a term with bindings *)
+
+let onInductionArg tac = function
+ | ElimOnConstr (c,lbindc as cbl) ->
+ if isVar c & lbindc = NoBindings then
+ tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl)
+ else
+ tac cbl
+ | ElimOnAnonHyp n ->
+ tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> tac (c,NoBindings)))
+ | ElimOnIdent (_,id) ->
+ (*Identifier apart because id can be quantified in goal and not typable*)
+ tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings))
+
(**************************)
(* Refinement tactics *)
(**************************)
@@ -2531,7 +2546,6 @@ let induct_destruct_l isrec with_evars lc elim names cls =
"'in' clause not supported when several induction hypothesis are given";
new_induct_gen_l isrec with_evars elim names newlc
-
(* Induction either over a term, over a quantified premisse, or over
several quantified premisses (like with functional induction
principles).
@@ -2540,19 +2554,10 @@ let induct_destruct_l isrec with_evars lc elim names cls =
let induct_destruct isrec with_evars lc elim names cls =
assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
if List.length lc = 1 then (* induction on one arg: use old mechanism *)
- try
- let c = List.hd lc in
- match c with
- | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c cls
- | ElimOnAnonHyp n ->
- tclTHEN (intros_until_n n)
- (tclLAST_HYP (fun c ->
- new_induct_gen isrec with_evars elim names (c,NoBindings) cls))
- (* Identifier apart because id can be quantified in goal and not typable *)
- | ElimOnIdent (_,id) ->
- tclTHEN (tclTRY (intros_until_id id))
- (new_induct_gen isrec with_evars elim names
- (mkVar id,NoBindings) cls)
+ try
+ onInductionArg
+ (fun c -> new_induct_gen isrec with_evars elim names c cls)
+ (List.hd lc)
with (* If this fails, try with new mechanism but if it fails too,
then the exception is the first one. *)
| x ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0492e296f..700c25f6e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -101,6 +101,13 @@ val intros_clearing : bool list -> tactic
val try_intros_until :
(identifier -> tactic) -> quantified_hypothesis -> tactic
+(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+ or a term with bindings *)
+
+val onInductionArg :
+ (constr with_ebindings -> tactic) ->
+ constr with_ebindings induction_arg -> tactic
+
(*s Introduction tactics with eliminations. *)
val intro_pattern : identifier option -> intro_pattern_expr -> tactic
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index f28c83deb..b57c54781 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -9,3 +9,26 @@ Qed.
Lemma l2 : forall H : 0 = 1, H = H.
discriminate H.
Qed.
+
+(* Check the variants of discriminate *)
+
+Goal O = S O -> True.
+discriminate 1.
+Undo.
+intros.
+discriminate H.
+Undo.
+Ltac g x := discriminate x.
+g H.
+Abort.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+try discriminate (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+ediscriminate (H O).
+instantiate (1:=O).
+Abort.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 606e884ae..867d73746 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -43,6 +43,29 @@ intros; injection H as Hyt Hxz.
exact Hxz.
Qed.
+(* Check the variants of injection *)
+
+Goal forall x y, S x = S y -> True.
+injection 1 as H'.
+Undo.
+intros.
+injection H as H'.
+Undo.
+Ltac f x := injection x.
+f H.
+Abort.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+try injection (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+einjection (H O).
+instantiate (1:=O).
+Abort.
+
(* Injection does not projects at positions in Prop... allow it?
Inductive t (A:Prop) : Set := c : A -> t A.
@@ -53,7 +76,7 @@ Abort.
*)
-(* Accept does not project on discriminable positions... allow it?
+(* Injection does not project on discriminable positions... allow it?
Goal 1=2 -> 1=0.
intro H.
@@ -61,4 +84,4 @@ injection H.
intro; assumption.
Qed.
- *)
+*)
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0ef835689..9192db722 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -525,7 +525,7 @@ let compute_bl_tact ind lnamesparrec nparrec =
intro_using freshz;
intros;
tclTRY (
- tclORELSE reflexivity (Equality.discr_tac None)
+ tclORELSE reflexivity (Equality.discr_tac false None)
);
simpl_in_hyp
((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
@@ -643,9 +643,10 @@ let compute_lb_tact ind lnamesparrec nparrec =
intro_using freshz;
intros;
tclTRY (
- tclORELSE reflexivity (Equality.discr_tac None)
+ tclORELSE reflexivity (Equality.discr_tac false None)
);
- Equality.inj [] freshz; intros; simpl_in_concl;
+ Equality.inj [] false (mkVar freshz,Rawterm.NoBindings);
+ intros; simpl_in_concl;
Auto.default_auto;
tclREPEAT (
tclTHENSEQ [apply (andb_true_intro());
@@ -806,6 +807,6 @@ let compute_dec_tact ind lnamesparrec nparrec =
Rawterm.NoBindings
)
true);
- Pfedit.by (Equality.discr_tac None)
+ Pfedit.by (Equality.discr_tac false None)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 03:12:42 +0000