aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/hiddentac.ml8
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/tacinterp.ml15
-rw-r--r--tactics/tactics.ml24
-rw-r--r--tactics/tactics.mli7
-rw-r--r--theories/Lists/List.v7
-rw-r--r--theories/Sorting/PermutSetoid.v2
-rw-r--r--theories/Sorting/Permutation.v15
-rw-r--r--toplevel/auto_ind_decl.ml2
10 files changed, 52 insertions, 34 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index daf97d5290..7417535217 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -722,7 +722,7 @@ let unify_resolve_nodelta (c,clenv) gl =
let unify_resolve flags (c,clenv) gl =
let clenv' = connect_clenv gl clenv in
let _ = clenv_unique_resolver false ~flags clenv' gl in
- h_apply true false [inj_open c,NoBindings] gl
+ h_apply true false [dummy_loc,(inj_open c,NoBindings)] gl
let unify_resolve_gen = function
| None -> unify_resolve_nodelta
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 65a56100bf..e6130cfcdc 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -40,10 +40,10 @@ let h_exact_no_check c =
let h_vm_cast_no_check c =
abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
let h_apply simple ev cb =
- abstract_tactic (TacApply (simple,ev,cb,None))
+ abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
(apply_with_ebindings_gen simple ev cb)
let h_apply_in simple ev cb (id,ipat as inhyp) =
- abstract_tactic (TacApply (simple,ev,cb,Some inhyp))
+ abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
(apply_in simple ev id cb ipat)
let h_elim ev cb cbo =
abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
@@ -131,8 +131,8 @@ let h_transitivity c =
abstract_tactic (TacTransitivity (Option.map inj_open c))
(intros_transitivity c)
-let h_simplest_apply c = h_apply false false [inj_open c,NoBindings]
-let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
+let h_simplest_apply c = h_apply false false [dummy_loc,(inj_open c,NoBindings)]
+let h_simplest_eapply c = h_apply false true [dummy_loc,(inj_open c,NoBindings)]
let h_simplest_elim c = h_elim false (c,NoBindings) None
let h_simplest_case c = h_case false (c,NoBindings)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f5b2dbb552..6f592108b1 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -38,9 +38,9 @@ val h_exact_no_check : constr -> tactic
val h_vm_cast_no_check : constr -> tactic
val h_apply : advanced_flag -> evars_flag ->
- open_constr with_bindings list -> tactic
+ open_constr with_bindings located list -> tactic
val h_apply_in : advanced_flag -> evars_flag ->
- open_constr with_bindings list ->
+ open_constr with_bindings located list ->
identifier * intro_pattern_expr located option -> tactic
val h_elim : evars_flag -> constr with_ebindings ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e436fc90f5..32c69ddcdc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1731,6 +1731,17 @@ let interp_constr_with_bindings ist gl (c,bl) =
let interp_open_constr_with_bindings ist gl (c,bl) =
(pf_interp_open_constr false ist gl c, interp_bindings ist gl bl)
+let loc_of_bindings = function
+| NoBindings -> dummy_loc
+| ImplicitBindings l -> loc_of_rawconstr (fst (list_last l))
+| ExplicitBindings l -> pi1 (list_last l)
+
+let interp_open_constr_with_bindings_loc ist gl ((c,_),bl as cb) =
+ let loc1 = loc_of_rawconstr c in
+ let loc2 = loc_of_bindings bl in
+ let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in
+ (loc,interp_open_constr_with_bindings ist gl cb)
+
let interp_induction_arg ist gl = function
| ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
| ElimOnAnonHyp n as x -> x
@@ -2230,9 +2241,9 @@ and interp_atomic ist gl = function
| TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
| TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
| TacApply (a,ev,cb,None) ->
- h_apply a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
+ h_apply a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb)
| TacApply (a,ev,cb,Some cl) ->
- h_apply_in a ev (List.map (interp_open_constr_with_bindings ist gl) cb)
+ h_apply_in a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb)
(interp_in_hyp_as ist gl cl)
| TacElim (ev,cb,cbo) ->
h_elim ev (interp_constr_with_bindings ist gl cb)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0224da6c87..ca64a8d3d2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -840,7 +840,7 @@ let check_evars sigma evm gl =
errorlabstrm "apply" (str"Uninstantiated existential variables: " ++
fnl () ++ pr_evar_defs rest)
-let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
+let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
let flags =
if with_delta then default_unify_flags else default_no_delta_unify_flags in
(* The actual type of the theorem. It will be matched against the
@@ -874,9 +874,9 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
if with_destruct then
descend_in_conjunctions with_evars
- try_main_apply (fun _ -> raise exn) c gl
+ try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl
else
- raise exn
+ Stdpp.raise_with_loc loc exn
in try_red_apply thm_ty0
in
if evm = Evd.empty then try_main_apply with_destruct c gl0
@@ -888,19 +888,18 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
let rec apply_with_ebindings_gen b e = function
| [] ->
tclIDTAC
- | [cb] ->
- general_apply b b e cb
+ | [cb] -> general_apply b b e cb
| cb::cbl ->
tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl)
-let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb]
-let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb]
+let apply_with_ebindings cb = apply_with_ebindings_gen false false [dloc,cb]
+let eapply_with_ebindings cb = apply_with_ebindings_gen false true [dloc,cb]
let apply_with_bindings (c,bl) =
apply_with_ebindings (inj_open c,inj_ebindings bl)
let eapply_with_bindings (c,bl) =
- apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl]
+ apply_with_ebindings_gen false true [dloc,(inj_open c,inj_ebindings bl)]
let apply c =
apply_with_ebindings (inj_open c,NoBindings)
@@ -947,7 +946,8 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
with NotExtensibleClause -> raise err in
aux (make_clenv_binding gl (d,thm) lbind)
-let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 =
+let apply_in_once with_delta with_destruct with_evars id
+ (loc,((sigma,d),lbind)) gl0 =
let flags =
if with_delta then default_unify_flags else default_no_delta_unify_flags in
let t' = pf_get_hyp_typ gl0 id in
@@ -1141,7 +1141,8 @@ let constructor_tac with_evars expctdnumopt i lbind gl =
Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
check_number_of_constructors expctdnumopt i nconstr;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in
+ let apply_tac =
+ general_apply true false with_evars (dloc,(inj_open cons,lbind)) in
(tclTHENLIST
[convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
@@ -1374,6 +1375,9 @@ let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl =
let apply_in simple with_evars = general_apply_in simple simple with_evars
+let simple_apply_in id c =
+ apply_in false false id [dloc,((Evd.empty,c),NoBindings)] None
+
(**************************)
(* Generalize tactics *)
(**************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 40740c3a82..6e52546f4a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -180,7 +180,8 @@ val apply : constr -> tactic
val eapply : constr -> tactic
val apply_with_ebindings_gen :
- advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
+ advanced_flag -> evars_flag -> open_constr with_ebindings located list ->
+ tactic
val apply_with_bindings : constr with_bindings -> tactic
val eapply_with_bindings : constr with_bindings -> tactic
@@ -192,9 +193,11 @@ val cut_and_apply : constr -> tactic
val apply_in :
advanced_flag -> evars_flag -> identifier ->
- open_constr with_ebindings list ->
+ open_constr with_ebindings located list ->
intro_pattern_expr located option -> tactic
+val simple_apply_in : identifier -> constr -> tactic
+
(*s Elimination tactics. *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 7e9711bba5..6582b2a872 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -785,11 +785,10 @@ Section ListOps.
End Reverse_Induction.
+ (*********************************************************************)
+ (** ** List permutations as a composition of adjacent transpositions *)
+ (*********************************************************************)
- (***********************************)
- (** ** Lists modulo permutation *)
- (***********************************)
-
Section Permutation.
Inductive Permutation : list A -> list A -> Prop :=
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 814ef0408d..1ea71972b5 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -13,7 +13,7 @@ Require Import Omega Relations Multiset Permutation SetoidList.
Set Implicit Arguments.
(** This file contains additional results about permutations
- with respect to an setoid equality (i.e. an equivalence relation).
+ with respect to a setoid equality (i.e. an equivalence relation).
*)
Section Perm.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index e9bbf88e3f..a922120545 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -12,22 +12,23 @@ Require Import Relations List Multiset Arith.
(** This file define a notion of permutation for lists, based on multisets:
there exists a permutation between two lists iff every elements have
- the same multiplicities in the two lists.
+ the same multiplicity in the two lists.
+
+ Unlike [List.Permutation], the present notion of permutation
+ requires the domain to be equipped with a decidable equality. This
+ equality allows to reason modulo the effective equivalence-class
+ representative used in each list.
- Unlike [List.Permutation], the present notion of permutation requires
- a decidable equality. At the same time, this definition can be used
- with a non-standard equality, whereas [List.Permutation] cannot.
-
The present file contains basic results, obtained without any particular
assumption on the decidable equality used.
-
+
File [PermutSetoid] contains additional results about permutations
with respect to an setoid equality (i.e. an equivalence relation).
Finally, file [PermutEq] concerns Coq equality : this file is similar
to the previous one, but proves in addition that [List.Permutation]
and [permutation] are equivalent in this context.
-x*)
+*)
Set Implicit Arguments.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 66d02278c3..5ddf2b7055 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -535,7 +535,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
tclREPEAT (
tclTHENSEQ [
- apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None;
+ simple_apply_in freshz (andb_prop());
fun gl ->
let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 08:56:38 +0000