aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/extraction/CHANGES4
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/funind/indfun_common.ml9
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/recdef.ml3
-rw-r--r--plugins/ltac/g_ltac.ml42
-rw-r--r--plugins/ltac/tacentries.ml4
-rw-r--r--plugins/setoid_ring/Field_theory.v6
-rw-r--r--plugins/setoid_ring/InitialRing.v24
-rw-r--r--plugins/setoid_ring/Ring_theory.v6
12 files changed, 53 insertions, 14 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 1524079f42..6d3d4b7432 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -10,7 +10,7 @@ open Context.Named.Declaration
let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
: Safe_typing.private_constants Entries.const_entry_body =
- Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
+ Future.chain x begin fun ((b,ctx),fx) ->
(f b , ctx) , fx
end
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index cf97ae3ab8..4bc3dba36e 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction:
* bug fixes:
- many concerning Records.
-- a Stack Overflow with mutual inductive (PR#320)
+- a Stack Overflow with mutual inductive (BZ#320)
- some optimizations have been removed since they were not type-safe:
For example if e has type: type 'x a = A
Then: match e with A -> A -----X----> e
@@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction:
- the dummy constant "__" have changed. see README
- - a few bug-fixes (#191 and others)
+ - a few bug-fixes (BZ#191 and others)
7.2 -> 7.3
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0f537abece..f708307c38 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -145,7 +145,7 @@ let rec pp_expr par env args =
| MLrel n ->
let id = get_db_name n env in
(* Try to survive to the occurrence of a Dummy rel.
- TODO: we should get rid of this hack (cf. #592) *)
+ TODO: we should get rid of this hack (cf. BZ#592) *)
let id = if Id.equal id dummy_name then Id.of_string "__" else id in
apply (Id.print id)
| MLapp (f,args') ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1e8854249a..76fcd5ec87 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -549,3 +549,12 @@ type tcc_lemma_value =
| Undefined
| Value of Term.constr
| Not_needed
+
+(* We only "purify" on exceptions *)
+let funind_purify f x =
+ let st = Vernacentries.freeze_interp_state `No in
+ try f x
+ with e ->
+ let e = CErrors.push e in
+ Vernacentries.unfreeze_interp_state st;
+ Exninfo.iraise e
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 2e2ced790e..d41abee87e 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -123,3 +123,5 @@ type tcc_lemma_value =
| Undefined
| Value of Term.constr
| Not_needed
+
+val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2997537664..9cb2a0a3f5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -759,7 +759,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let funs = Array.of_list funs and graphs = Array.of_list graphs in
let map (c, u) = mkConstU (c, EInstance.make u) in
let funs_constr = Array.map map funs in
- States.with_state_protection_on_exception
+ (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ funind_purify
(fun () ->
let env = Global.env () in
let evd = ref (Evd.from_env env) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 74c454334e..76f859ed72 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1595,7 +1595,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
spc () ++ str"is defined" )
)
in
- States.with_state_protection_on_exception (fun () ->
+ (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ funind_purify (fun () ->
com_terminate
tcc_lemma_name
tcc_lemma_constr
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index d639dd0e1c..c577cb2198 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -340,7 +340,7 @@ GEXTEND Gram
command:
[ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
- Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l)
+ Vernacexpr.VernacProof (Some (in_tac ta), l)
| IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] ->
Vernacexpr.VernacProof (ta,Some l) ] ]
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index bcd5b388a1..0bf6e3d155 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -468,7 +468,9 @@ let register_ltac local tacl =
let () = List.iter iter_rec recvars in
List.map map rfun
in
- let defs = Future.transactify defs () in
+ (* STATE XXX: Review what is going on here. Why does this needs
+ protection? Why is not the STM level protection enough? Fishy *)
+ let defs = States.with_state_protection defs () in
let iter (def, tac) = match def with
| NewTac id ->
Tacenv.register_ltac false local id tac;
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 88e2cb1da5..462ffde313 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1612,7 +1612,11 @@ Section Complete.
Notation "x / y " := (rdiv x y). Notation "/ x" := (rinv x).
Notation "x == y" := (req x y) (at level 70, no associativity).
Variable Rsth : Setoid_Theory R req.
- Add Setoid R req Rsth as R_setoid3.
+ Add Parametric Relation : R req
+ reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
+ symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
+ transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ as R_setoid3.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
Proof. exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index bd4e94687d..8aa0b1c91f 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -48,7 +48,11 @@ Section ZMORPHISM.
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
- Add Setoid R req Rsth as R_setoid3.
+ Add Parametric Relation : R req
+ reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
+ symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
+ transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ as R_setoid3.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
@@ -260,7 +264,11 @@ Section NMORPHISM.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Variable Rsth : Setoid_Theory R req.
- Add Setoid R req Rsth as R_setoid4.
+ Add Parametric Relation : R req
+ reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
+ symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
+ transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ as R_setoid4.
Ltac rrefl := gen_reflexivity Rsth.
Variable SReqe : sring_eq_ext radd rmul req.
Variable SRth : semi_ring_theory 0 1 radd rmul req.
@@ -381,7 +389,11 @@ Section NWORDMORPHISM.
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
- Add Setoid R req Rsth as R_setoid5.
+ Add Parametric Relation : R req
+ reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
+ symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
+ transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ as R_setoid5.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
@@ -566,7 +578,11 @@ Section GEN_DIV.
Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.
(* Useful tactics *)
- Add Setoid R req Rsth as R_set1.
+ Add Parametric Relation : R req
+ reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
+ symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
+ transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
Proof. exact (Radd_ext Reqe). Qed.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 335a68d70f..776ebd808d 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -404,7 +404,11 @@ Section ALMOST_RING.
Variable Csth : Equivalence ceq.
Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
- Add Setoid C ceq Csth as C_setoid.
+ Add Parametric Relation : C ceq
+ reflexivity proved by Csth.(@Equivalence_Reflexive _ _)
+ symmetry proved by Csth.(@Equivalence_Symmetric _ _)
+ transitivity proved by Csth.(@Equivalence_Transitive _ _)
+ as C_setoid.
Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
Proof. exact (Radd_ext Ceqe). Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 05:31:38 +0000