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.ml6
-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, 46 insertions, 46 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..62556d38ff 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
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 11:02:16 +0000