aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml4
-rw-r--r--stm/asyncTaskQueue.mli4
-rw-r--r--stm/coqworkmgrApi.ml4
-rw-r--r--stm/coqworkmgrApi.mli4
-rw-r--r--stm/dag.ml4
-rw-r--r--stm/dag.mli4
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/proofBlockDelimiter.mli4
-rw-r--r--stm/spawned.ml4
-rw-r--r--stm/spawned.mli4
-rw-r--r--stm/stm.ml34
-rw-r--r--stm/stm.mli4
-rw-r--r--stm/tQueue.ml4
-rw-r--r--stm/tQueue.mli4
-rw-r--r--stm/vcs.ml4
-rw-r--r--stm/vcs.mli4
-rw-r--r--stm/vernac_classifier.ml6
-rw-r--r--stm/vernac_classifier.mli4
-rw-r--r--stm/vio_checking.ml4
-rw-r--r--stm/vio_checking.mli4
-rw-r--r--stm/workerPool.ml4
-rw-r--r--stm/workerPool.mli4
22 files changed, 61 insertions, 59 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 9eb0924bd6..c8eb7b08f1 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index e6cf6343c8..cf174d0c93 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 2b39a7a2aa..008d0ac4ce 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 29eba5bc91..baa199aee1 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/dag.ml b/stm/dag.ml
index 4504de681b..9df1cfd65d 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/dag.mli b/stm/dag.mli
index 1cd593fdad..3ab34041d0 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 0e8c463b19..6a78dd5529 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index e45f489a38..2166a0d60a 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 916139884b..5cc8be78f5 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/spawned.mli b/stm/spawned.mli
index 36612b1450..bd022aff97 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/stm.ml b/stm/stm.ml
index a5b868343d..5b88ee3d68 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -878,7 +878,7 @@ end = struct (* {{{ *)
Vernacstate.LemmaStack.t option *
int * (* Evarutil.meta_counter_summary_tag *)
int * (* Evd.evar_counter_summary_tag *)
- DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+ DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
type partial_state =
[ `Full of Vernacstate.t
@@ -1501,7 +1501,7 @@ end = struct (* {{{ *)
let wall_clock2 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
- let p = PG_compat.return_proof ~allow_partial:drop_pt () in
+ let p = if drop_pt then PG_compat.return_partial_proof () else PG_compat.return_proof () in
if drop_pt then feedback ~id Complete;
p)
@@ -1522,15 +1522,15 @@ end = struct (* {{{ *)
let st = State.freeze () in
if not drop then begin
let checked_proof = Future.chain future_proof (fun p ->
- let opaque = Proof_global.Opaque in
(* Unfortunately close_future_proof and friends are not pure so we need
to set the state manually here *)
State.unfreeze st;
let pobject, _info =
- PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+ PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ let opaque = Proof_global.Opaque in
stm_qed_delay_proof ~st ~id:stop
~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
ignore(Future.join checked_proof);
@@ -1661,14 +1661,14 @@ end = struct (* {{{ *)
try
Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
if drop then
- let _proof = PG_compat.return_proof ~allow_partial:true () in
+ let _proof = PG_compat.return_partial_proof () in
`OK_ADMITTED
else begin
let opaque = Proof_global.Opaque in
(* The original terminator, a hook, has not been saved in the .vio*)
let proof, _info =
- PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
+ PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
let info = Lemmas.Info.make () in
@@ -2479,13 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
~drop_pt exn_info block_stop, ref false
in
qed.fproof <- Some (Some fp, cancel);
- let opaque = match keep' with
- | VtKeepAxiom | VtKeepOpaque ->
- Proof_global.Opaque (* Admitted -> Opaque should be OK. *)
- | VtKeepDefined -> Proof_global.Transparent
+ let () = match keep' with
+ | VtKeepAxiom | VtKeepOpaque -> ()
+ | VtKeepDefined ->
+ CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.")
in
let proof, info =
- PG_compat.close_future_proof ~opaque ~feedback_id:id fp in
+ PG_compat.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
@@ -2518,9 +2518,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
| VtKeepAxiom -> assert false
in
- Some(PG_compat.close_proof ~opaque
- ~keep_body_ucst_separate:false
- (State.exn_on id ~valid:eop)) in
+ try Some (PG_compat.close_proof ~opaque ~keep_body_ucst_separate:false)
+ with exn ->
+ let iexn = Exninfo.capture exn in
+ Exninfo.iraise (State.exn_on id ~valid:eop iexn)
+ in
if keep <> VtKeep VtKeepAxiom then
reach view.next;
let wall_clock2 = Unix.gettimeofday () in
diff --git a/stm/stm.mli b/stm/stm.mli
index e56bac6e0f..2c27d63b82 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 72a40a2a9c..e17c3a2f88 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index c8c592e42f..12fa907945 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vcs.ml b/stm/vcs.ml
index 26be9ae76f..4cf040b44c 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vcs.mli b/stm/vcs.mli
index 584560f833..75900aa027 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 65ef2ca8c6..567acb1c73 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -130,7 +130,7 @@ let classify_vernac e =
| VernacPrimitive (id,_,_) ->
VtSideff ([id.CAst.v], VtLater)
| VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
- | VernacInductive (_, _,_,l) ->
+ | VernacInductive (_,l) ->
let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 77994fac2e..61bf3a503a 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 837ba3d880..446664e531 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli
index 0f139921ef..73036762a3 100644
--- a/stm/vio_checking.mli
+++ b/stm/vio_checking.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index d82741576e..45c92c3748 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index 88175a788c..18b8c6bf49 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:42:59 +0000