aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml20
-rw-r--r--API/API.mli17
-rw-r--r--CHANGES2
-rw-r--r--README.md2
-rw-r--r--dev/ci/ci-basic-overlay.sh11
-rw-r--r--dev/doc/changes.md6
-rw-r--r--kernel/context.ml5
-rw-r--r--plugins/funind/invfun.ml9
-rw-r--r--plugins/ltac/extratactics.ml430
-rw-r--r--plugins/ltac/tactic_matching.ml2
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--printing/prettyp.ml5
-rw-r--r--tactics/eqdecide.ml8
-rw-r--r--tactics/equality.ml98
-rw-r--r--tactics/equality.mli24
-rw-r--r--tactics/inv.ml2
-rw-r--r--test-suite/bugs/closed/1238.v (renamed from test-suite/bugs/closed/38.v)0
-rw-r--r--test-suite/bugs/closed/1341.v (renamed from test-suite/bugs/closed/121.v)0
-rw-r--r--test-suite/bugs/closed/1362.v (renamed from test-suite/bugs/closed/148.v)0
-rw-r--r--test-suite/bugs/closed/1542.v (renamed from test-suite/bugs/closed/328.v)0
-rw-r--r--test-suite/bugs/closed/1543.v (renamed from test-suite/bugs/closed/329.v)0
-rw-r--r--test-suite/bugs/closed/1545.v (renamed from test-suite/bugs/closed/331.v)0
-rw-r--r--test-suite/bugs/closed/1547.v (renamed from test-suite/bugs/closed/335.v)0
-rw-r--r--test-suite/bugs/closed/1551.v (renamed from test-suite/bugs/closed/348.v)0
-rw-r--r--test-suite/bugs/closed/1584.v (renamed from test-suite/bugs/closed/545.v)0
-rw-r--r--test-suite/bugs/closed/5281.v6
-rw-r--r--test-suite/bugs/closed/5797.v (renamed from test-suite/bugs/closed/846.v)0
-rw-r--r--test-suite/bugs/closed/5845.v (renamed from test-suite/bugs/closed/931.v)0
-rw-r--r--test-suite/bugs/closed/5940.v (renamed from test-suite/bugs/closed/1100.v)0
-rw-r--r--test-suite/bugs/opened/1615.v (renamed from test-suite/bugs/opened/743.v)0
-rw-r--r--theories/QArith/QArith_base.v20
-rw-r--r--theories/QArith/Qabs.v7
-rw-r--r--vernac/auto_ind_decl.ml17
-rw-r--r--vernac/record.ml1
34 files changed, 198 insertions, 96 deletions
diff --git a/.travis.yml b/.travis.yml
index 196f4b22ad..8d70e346ad 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,6 +39,7 @@ env:
- TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
- TEST_TARGET="validate" TW="travis_wait"
- TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
+ - TEST_TARGET="validate" COMPILER="4.05.0+flambda" CAMLP5_VER="7.01" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" NATIVE_COMP="no"
- TEST_TARGET="ci-bignums TIMED=1"
- TEST_TARGET="ci-color TIMED=1"
- TEST_TARGET="ci-compcert TIMED=1"
@@ -103,6 +104,21 @@ matrix:
- avsm
packages: *extra-packages
+ # Full test-suite with flambda
+ - env:
+ - TEST_TARGET="test-suite"
+ - COMPILER="4.05.0+flambda"
+ - FINDLIB_VER="1.7.3"
+ - CAMLP5_VER="7.01"
+ - NATIVE_COMP="no"
+ - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
+ - EXTRA_OPAM="lablgtk-extras hevea"
+ addons:
+ apt:
+ sources:
+ - avsm
+ packages: *extra-packages
+
# Ocaml warnings with two compilers
- env:
- TEST_TARGET="coqocaml"
@@ -143,7 +159,7 @@ matrix:
- NATIVE_COMP="no"
- COQ_DEST="-local"
before_install:
- - brew update --debug --verbose
+ - brew update
- brew install opam gnu-time
- if: NOT (type = pull_request)
@@ -157,7 +173,7 @@ matrix:
- EXTRA_CONF="-coqide opt -warn-error"
- EXTRA_OPAM="lablgtk-extras"
before_install:
- - brew update --debug --verbose
+ - brew update
- brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3
- pip3 install macpack
before_deploy:
diff --git a/API/API.mli b/API/API.mli
index a41009fa2f..5e41464c80 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5337,6 +5337,11 @@ sig
| Naive
| FirstSolved
| AllMatches
+ type inj_flags = {
+ keep_proof_equalities : bool; (* One may want it or not *)
+ injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *)
+ injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
+ }
val build_selector :
Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
@@ -5345,20 +5350,20 @@ sig
val general_rewrite :
orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic
- val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
+ val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic
val general_multi_rewrite :
Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list ->
Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic
val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic
- val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
+ val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
val discr_tac : Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
- val injClause : Tactypes.intro_patterns option -> Misctypes.evars_flag ->
+ val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic
- val simpleInjClause : Misctypes.evars_flag ->
+ val simpleInjClause : inj_flags option -> Misctypes.evars_flag ->
EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option ->
unit Proofview.tactic
val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic
@@ -5392,8 +5397,8 @@ sig
?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic
val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val discrHyp : Names.Id.t -> unit Proofview.tactic
- val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
- val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
+ val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool
+ val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic
val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic
end
diff --git a/CHANGES b/CHANGES
index 640ab4aa50..7a326c589a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,8 @@ Tactics
such as "x := 5 : Z" (see BZ#148). This could be disabled via
Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
+- Tactic "decide equality" now able to manage constructors which
+ contain proofs.
Changes from 8.7+beta2 to 8.7.0
===============================
diff --git a/README.md b/README.md
index 03f24071b8..2ad5122156 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
# Coq
-[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) [![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
+[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) [![Build status](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master) [![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 545846da58..9be882bb3c 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -49,11 +49,8 @@
########################################################################
# HoTT
########################################################################
-# Temporary overlay
-: ${HoTT_CI_BRANCH:=ocaml.4.02.3}
-: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
-# : ${HoTT_CI_BRANCH:=master}
-# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
+: ${HoTT_CI_BRANCH:=master}
+: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
########################################################################
# GeoCoq
@@ -76,8 +73,8 @@
########################################################################
# CompCert
########################################################################
-: ${CompCert_CI_BRANCH:=less_init_plugins}
-: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
+: ${CompCert_CI_BRANCH:=master}
+: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
########################################################################
# VST
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 8a2a2fffc6..6ade6576f7 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -32,6 +32,12 @@ We renamed the following datatypes:
- `Pp.std_ppcmds` -> `Pp.t`
+Some tactics and related functions now support static configurability, e.g.:
+
+- injectable, dEq, etc. takes an argument ~keep_proofs which,
+ - if None, tells to behave as told with the flag Keep Proof Equalities
+ - if Some b, tells to keep proof equalities iff b is true
+
## Changes between Coq 8.6 and Coq 8.7
### Ocaml
diff --git a/kernel/context.ml b/kernel/context.ml
index 929324efec..d635c4515b 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -379,8 +379,9 @@ struct
(** Return the number of {e local declarations} in a given named-context. *)
let length = List.length
-(** Return a declaration designated by a given de Bruijn index.
- @raise Not_found if the designated identifier is not present in the designated named-context. *) let rec lookup id = function
+(** Return a declaration designated by a given identifier
+ @raise Not_found if the designated identifier is not present in the designated named-context. *)
+ let rec lookup id = function
| decl :: _ when Id.equal id (Declaration.get_id decl) -> decl
| _ :: sign -> lookup id sign
| [] -> raise Not_found
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9cb2a0a3f5..93317fce1b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -570,6 +570,11 @@ let rec reflexivity_with_destruct_cases g =
with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
let eq_ind = make_eq () in
+ let my_inj_flags = Some {
+ Equality.keep_proof_equalities = false;
+ injection_in_context = false; (* for compatibility, necessary *)
+ injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *)
+ } in
let discr_inject =
Tacticals.onAllHypsAndConcl (
fun sc g ->
@@ -580,8 +585,8 @@ let rec reflexivity_with_destruct_cases g =
| App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
- else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
+ else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
+ then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a7aebf9e15..65c186a419 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c =
(fun c -> tac with_evars (Some (None,ElimOnConstr c)))
TACTIC EXTEND simplify_eq
- [ "simplify_eq" ] -> [ dEq false None ]
-| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ]
+ [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
+| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
END
TACTIC EXTEND esimplify_eq
-| [ "esimplify_eq" ] -> [ dEq true None ]
-| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
+| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
+| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
END
let discr_main c = elimOnConstrWithHoles discr_tac false c
@@ -117,31 +117,31 @@ let discrHyp id =
discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
let injection_main with_evars c =
- elimOnConstrWithHoles (injClause None) with_evars c
+ elimOnConstrWithHoles (injClause None None) with_evars c
TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause None false None ]
-| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
+| [ "injection" ] -> [ injClause None None false None ]
+| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
END
TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause None true None ]
-| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
+| [ "einjection" ] -> [ injClause None None true None ]
+| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
END
TACTIC EXTEND injection_as
| [ "injection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) false None ]
+ [ injClause None (Some ipat) false None ]
| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) false c ]
+ [ mytclWithHoles (injClause None (Some ipat)) false c ]
END
TACTIC EXTEND einjection_as
| [ "einjection" "as" intropattern_list(ipat)] ->
- [ injClause (Some ipat) true None ]
+ [ injClause None (Some ipat) true None ]
| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- [ mytclWithHoles (injClause (Some ipat)) true c ]
+ [ mytclWithHoles (injClause None (Some ipat)) true c ]
END
TACTIC EXTEND simple_injection
-| [ "simple" "injection" ] -> [ simpleInjClause false None ]
-| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
+| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
+| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
END
let injHyp id =
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 63b8cc4824..18bb7d2dbd 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -203,7 +203,7 @@ module PatternMatching (E:StaticEnvironment) = struct
let pick l = pick l imatching_error
- (** Declares a subsitution, a context substitution and a term substitution. *)
+ (** Declares a substitution, a context substitution and a term substitution. *)
let put subst context terms : unit m =
let s = { subst ; context ; terms ; lhs = () } in
{ stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 832044909c..26b5c57675 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -396,7 +396,7 @@ let revtoptac n0 gl =
let equality_inj l b id c gl =
let msg = ref "" in
- try Proofview.V82.of_tactic (Equality.inj l b None c) gl
+ try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
| Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2077526db4..fdaeded878 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -807,7 +807,8 @@ let print_any_name = function
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,str = repr_qualid qid in
if not (DirPath.is_empty dir) then raise Not_found;
- str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl
+ str |> Global.lookup_named |> print_named_decl
+
with Not_found ->
user_err
~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
@@ -839,7 +840,7 @@ let print_opaque_name qid =
let open EConstr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
- env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
+ env |> lookup_named id |> print_named_decl
let print_about_any ?loc k =
match k with
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d912decff4..8764ef085d 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) =
clear_last;
intros]
+let inj_flags = Some {
+ Equality.keep_proof_equalities = true; (* necessary *)
+ Equality.injection_in_context = true; (* does not matter here *)
+ Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+ }
+
let discrHyp id =
let c env sigma = (sigma, (mkVar id, NoBindings)) in
let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
@@ -136,7 +142,7 @@ let eqCase tac =
let injHyp id =
let c env sigma = (sigma, (mkVar id, NoBindings)) in
- let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
+ let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
let diseqCase hyps eqonleft =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e33dd2e5ed..7c03a3ba6a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -48,6 +48,12 @@ module NamedDecl = Context.Named.Declaration
(* Options *)
+type inj_flags = {
+ keep_proof_equalities : bool;
+ injection_in_context : bool;
+ injection_pattern_l2r_order : bool;
+ }
+
let discriminate_introduction = ref true
let discr_do_intro () = !discriminate_introduction
@@ -63,7 +69,9 @@ let _ =
let injection_pattern_l2r_order = ref true
-let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
+let use_injection_pattern_l2r_order = function
+ | None -> !injection_pattern_l2r_order
+ | Some flags -> flags.injection_pattern_l2r_order
let _ =
declare_bool_option
@@ -75,9 +83,9 @@ let _ =
let injection_in_context = ref false
-let use_injection_in_context () =
- !injection_in_context
- && Flags.version_strictly_greater Flags.V8_5
+let use_injection_in_context = function
+ | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5
+ | Some flags -> flags.injection_in_context
let _ =
declare_bool_option
@@ -721,7 +729,14 @@ let _ =
optread = (fun () -> !keep_proof_equalities_for_injection) ;
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
-let find_positions env sigma ~no_discr t1 t2 =
+let keep_proof_equalities = function
+ | None -> !keep_proof_equalities_for_injection
+ | Some flags -> flags.keep_proof_equalities
+
+(* [keep_proofs] is relevant for types in Prop with elimination in Type *)
+(* In particular, it is relevant for injection but not for discriminate *)
+
+let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
let project env sorts posn t1 t2 =
let ty1 = get_type_of env sigma t1 in
let s = get_sort_family_of env sigma ty1 in
@@ -768,20 +783,22 @@ let find_positions env sigma ~no_discr t1 t2 =
project env sorts posn t1_0 t2_0
in
try
- let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
- else [InSet;InType]
- in
+ let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in
Inr (findrec sorts [] t1 t2)
with DiscrFound (path,c1,c2) ->
Inl (path,c1,c2)
+let use_keep_proofs = function
+ | None -> !keep_proof_equalities_for_injection
+ | Some b -> b
+
let discriminable env sigma t1 t2 =
- match find_positions env sigma ~no_discr:false t1 t2 with
+ match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inl _ -> true
| _ -> false
-let injectable env sigma t1 t2 =
- match find_positions env sigma ~no_discr:true t1 t2 with
+let injectable env sigma ~keep_proofs t1 t2 =
+ match find_positions env sigma ~keep_proofs:(use_keep_proofs keep_proofs) ~no_discr:true t1 t2 with
| Inl _ -> assert false
| Inr [] | Inr [([],_,_)] -> false
| Inr _ -> true
@@ -1024,7 +1041,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- match find_positions env sigma ~no_discr:false t1 t2 with
+ match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inr _ ->
tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
@@ -1069,9 +1086,8 @@ let discr with_evars = onEquality with_evars discrEq
let discrClause with_evars = onClause (discrSimpleClause with_evars)
let discrEverywhere with_evars =
-(*
- tclORELSE
-*)
+ tclTHEN (Proofview.tclUNIT ())
+ (* Delay the interpretation of side-effect *)
(if discr_do_intro () then
(tclTHEN
(tclREPEAT introf)
@@ -1079,9 +1095,7 @@ let discrEverywhere with_evars =
(fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
else (* <= 8.2 compat *)
tryAllHypsAndConcl (discrSimpleClause with_evars))
-(* (fun gls ->
- user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities."))
-*)
+
let discr_tac with_evars = function
| None -> discrEverywhere with_evars
| Some c -> onInductionArg (fun clear_flag -> discr with_evars) c
@@ -1403,15 +1417,15 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))
-let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
- match find_positions env sigma ~no_discr:true t1 t2 with
+ match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with
| Inl _ ->
assert false
| Inr [] ->
let suggestion =
- if !keep_proof_equalities_for_injection then
+ if keep_proofs then
"" else
" You can try to use option Set Keep Proof Equalities." in
tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
@@ -1430,13 +1444,13 @@ let get_previous_hyp_position id gl =
in
aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
-let injEq ?(old=false) with_evars clear_flag ipats =
+let injEq flags ?(old=false) with_evars clear_flag ipats =
(* Decide which compatibility mode to use *)
let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with
- | None when not old && use_injection_in_context () ->
+ | None when not old && use_injection_in_context flags ->
Some [], true, true, true
| None -> None, false, false, false
- | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in
+ | _ -> let b = use_injection_pattern_l2r_order flags in ipats, b, b, b in
(* Built the post tactic depending on compatibility mode *)
let post_tac c n =
match ipats_style with
@@ -1456,26 +1470,26 @@ let injEq ?(old=false) with_evars clear_flag ipats =
tclTHEN clear_tac intro_tac
end
| None -> tclIDTAC in
- injEqThen post_tac l2r
+ injEqThen (keep_proof_equalities flags) post_tac l2r
-let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
+let inj flags ipats with_evars clear_flag = onEquality with_evars (injEq flags with_evars clear_flag ipats)
-let injClause ipats with_evars = function
- | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
- | Some c -> onInductionArg (inj ipats with_evars) c
+let injClause flags ipats with_evars = function
+ | None -> onNegatedEquality with_evars (injEq flags with_evars None ipats)
+ | Some c -> onInductionArg (inj flags ipats with_evars) c
-let simpleInjClause with_evars = function
- | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None)
- | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
+let simpleInjClause flags with_evars = function
+ | None -> onNegatedEquality with_evars (injEq flags ~old:true with_evars None None)
+ | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c
-let injConcl = injClause None false None
-let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
+let injConcl flags = injClause flags None false None
+let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
-let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
+let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
Proofview.Goal.enter begin fun gl ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
- match find_positions env sigma ~no_discr:false t1 t2 with
+ match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
@@ -1485,18 +1499,18 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
(ntac (clenv_value clause))
end
-let dEqThen with_evars ntac = function
- | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
- | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c
+let dEqThen ~keep_proofs with_evars ntac = function
+ | None -> onNegatedEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac None))
+ | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac clear_flag))) c
-let dEq with_evars =
- dEqThen with_evars (fun clear_flag c x ->
+let dEq ~keep_proofs with_evars =
+ dEqThen ~keep_proofs with_evars (fun clear_flag c x ->
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decomp_eq tac data (c, t) =
Proofview.Goal.enter begin fun gl ->
let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
- decompEqThen (fun _ -> tac) data cl
+ decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl
end
let _ = declare_intro_decomp_eq intro_decomp_eq
diff --git a/tactics/equality.mli b/tactics/equality.mli
index a4d1c0f9bd..65da2e7dc0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -67,23 +67,31 @@ val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.ta
val replace : constr -> constr -> unit Proofview.tactic
val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
+type inj_flags = {
+ keep_proof_equalities : bool; (* One may want it or not *)
+ injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *)
+ injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
+ }
+
val discr : evars_flag -> constr with_bindings -> unit Proofview.tactic
val discrConcl : unit Proofview.tactic
val discrHyp : Id.t -> unit Proofview.tactic
val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
constr with_bindings destruction_arg option -> unit Proofview.tactic
-val inj : intro_patterns option -> evars_flag ->
+
+(* Below, if flag is [None], it takes the value from the dynamic value of the option *)
+val inj : inj_flags option -> intro_patterns option -> evars_flag ->
clear_flag -> constr with_bindings -> unit Proofview.tactic
-val injClause : intro_patterns option -> evars_flag ->
+val injClause : inj_flags option -> intro_patterns option -> evars_flag ->
constr with_bindings destruction_arg option -> unit Proofview.tactic
-val injHyp : clear_flag -> Id.t -> unit Proofview.tactic
-val injConcl : unit Proofview.tactic
-val simpleInjClause : evars_flag ->
+val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic
+val injConcl : inj_flags option -> unit Proofview.tactic
+val simpleInjClause : inj_flags option -> evars_flag ->
constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
@@ -100,7 +108,7 @@ val rewriteInConcl : bool -> constr -> unit Proofview.tactic
val discriminable : env -> evar_map -> constr -> constr -> bool
(* Tells if tactic "injection" is applicable *)
-val injectable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> keep_proofs:(bool option) -> constr -> constr -> bool
(* Subst *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f391382bfc..c5aa74ba5c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -371,7 +371,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
(* If no immediate variable in the equation, try to decompose it *)
(* and apply a trailer which again try to substitute *)
(fun id ->
- dEqThen false (deq_trailer id)
+ dEqThen ~keep_proofs:None false (deq_trailer id)
(Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings))))
id
diff --git a/test-suite/bugs/closed/38.v b/test-suite/bugs/closed/1238.v
index 6b6e83779f..6b6e83779f 100644
--- a/test-suite/bugs/closed/38.v
+++ b/test-suite/bugs/closed/1238.v
diff --git a/test-suite/bugs/closed/121.v b/test-suite/bugs/closed/1341.v
index 8c5a38859f..8c5a38859f 100644
--- a/test-suite/bugs/closed/121.v
+++ b/test-suite/bugs/closed/1341.v
diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/1362.v
index 6cafb9f0cd..6cafb9f0cd 100644
--- a/test-suite/bugs/closed/148.v
+++ b/test-suite/bugs/closed/1362.v
diff --git a/test-suite/bugs/closed/328.v b/test-suite/bugs/closed/1542.v
index 52cfbbc496..52cfbbc496 100644
--- a/test-suite/bugs/closed/328.v
+++ b/test-suite/bugs/closed/1542.v
diff --git a/test-suite/bugs/closed/329.v b/test-suite/bugs/closed/1543.v
index def6ed98dd..def6ed98dd 100644
--- a/test-suite/bugs/closed/329.v
+++ b/test-suite/bugs/closed/1543.v
diff --git a/test-suite/bugs/closed/331.v b/test-suite/bugs/closed/1545.v
index 9ef796faf7..9ef796faf7 100644
--- a/test-suite/bugs/closed/331.v
+++ b/test-suite/bugs/closed/1545.v
diff --git a/test-suite/bugs/closed/335.v b/test-suite/bugs/closed/1547.v
index 166fa7a9f2..166fa7a9f2 100644
--- a/test-suite/bugs/closed/335.v
+++ b/test-suite/bugs/closed/1547.v
diff --git a/test-suite/bugs/closed/348.v b/test-suite/bugs/closed/1551.v
index 48f0b55129..48f0b55129 100644
--- a/test-suite/bugs/closed/348.v
+++ b/test-suite/bugs/closed/1551.v
diff --git a/test-suite/bugs/closed/545.v b/test-suite/bugs/closed/1584.v
index 926af7dd1c..926af7dd1c 100644
--- a/test-suite/bugs/closed/545.v
+++ b/test-suite/bugs/closed/1584.v
diff --git a/test-suite/bugs/closed/5281.v b/test-suite/bugs/closed/5281.v
new file mode 100644
index 0000000000..03bafdc9ae
--- /dev/null
+++ b/test-suite/bugs/closed/5281.v
@@ -0,0 +1,6 @@
+Inductive A (T : Prop) := B (_ : T).
+Scheme Equality for A.
+
+Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}.
+decide equality.
+Qed.
diff --git a/test-suite/bugs/closed/846.v b/test-suite/bugs/closed/5797.v
index ee5ec1fa6a..ee5ec1fa6a 100644
--- a/test-suite/bugs/closed/846.v
+++ b/test-suite/bugs/closed/5797.v
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/5845.v
index ea3347a851..ea3347a851 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/5845.v
diff --git a/test-suite/bugs/closed/1100.v b/test-suite/bugs/closed/5940.v
index 32c78b4b9e..32c78b4b9e 100644
--- a/test-suite/bugs/closed/1100.v
+++ b/test-suite/bugs/closed/5940.v
diff --git a/test-suite/bugs/opened/743.v b/test-suite/bugs/opened/1615.v
index 2825701410..2825701410 100644
--- a/test-suite/bugs/opened/743.v
+++ b/test-suite/bugs/opened/1615.v
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index a19f9f9025..5996d30f25 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -171,6 +171,26 @@ Proof.
auto with qarith.
Qed.
+Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x.
+Proof.
+ apply eq_true_iff_eq. rewrite !Qeq_bool_iff. now symmetry.
+Qed.
+
+Lemma Qeq_bool_refl x: Qeq_bool x x = true.
+Proof.
+ rewrite Qeq_bool_iff. now reflexivity.
+Qed.
+
+Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true.
+Proof.
+ rewrite !Qeq_bool_iff. now symmetry.
+Qed.
+
+Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.
+Proof.
+ rewrite !Qeq_bool_iff; apply Qeq_trans.
+Qed.
+
Hint Resolve Qnot_eq_sym : qarith.
(** * Addition, multiplication and opposite *)
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 116aa0d429..ec2ac7832d 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -100,6 +100,13 @@ rewrite Z.abs_mul.
reflexivity.
Qed.
+Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q).
+Proof.
+ intros [n d]; simpl.
+ unfold Qinv.
+ case_eq n; intros; simpl in *; apply Qeq_refl.
+Qed.
+
Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x).
Proof.
unfold Qminus, Qopp. simpl.
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 503508fc04..7af391758d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -91,6 +91,15 @@ let destruct_on_using c id =
let destruct_on_as c l =
destruct false None c (Some (Loc.tag l)) None
+let inj_flags = Some {
+ Equality.keep_proof_equalities = true; (* necessary *)
+ injection_in_context = true; (* does not matter here *)
+ Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+ }
+
+let my_discr_tac = Equality.discr_tac false None
+let my_inj_tac x = Equality.inj inj_flags None false None (EConstr.mkVar x,NoBindings)
+
(* reconstruct the inductive with the correct de Bruijn indexes *)
let mkFullInd (ind,u) n =
let mib = Global.lookup_mind (fst ind) in
@@ -595,7 +604,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
intro_using freshz;
intros;
Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
);
simpl_in_hyp (freshz,Locus.InHyp);
(*
@@ -739,9 +748,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
intro_using freshz;
intros;
Tacticals.New.tclTRY (
- Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
+ Tacticals.New.tclORELSE reflexivity my_discr_tac
);
- Equality.inj None false None (EConstr.mkVar freshz,NoBindings);
+ my_inj_tac freshz;
intros; simpl_in_concl;
Auto.default_auto;
Tacticals.New.tclREPEAT (
@@ -936,7 +945,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
NoBindings
)
true;
- Equality.discr_tac false None
+ my_discr_tac
]
end
]
diff --git a/vernac/record.ml b/vernac/record.ml
index 9a8657c3c3..5533fe5b38 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -418,7 +418,6 @@ let declare_structure finite univs id idbuild paramimpls params arity template
begin
let env = Global.env () in
let env' = Environ.push_context ctx env in
- (* let env'' = Environ.push_rel_context params env' in *)
let evd = Evd.from_env env' in
Inductiveops.infer_inductive_subtyping env' evd mie
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:12:21 +0000