aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--stm/asyncTaskQueue.mli2
-rw-r--r--stm/coqworkmgrApi.ml2
-rw-r--r--stm/coqworkmgrApi.mli2
-rw-r--r--stm/dag.ml2
-rw-r--r--stm/dag.mli2
-rw-r--r--stm/proofBlockDelimiter.ml2
-rw-r--r--stm/proofBlockDelimiter.mli2
-rw-r--r--stm/proofworkertop.ml2
-rw-r--r--stm/queryworkertop.ml2
-rw-r--r--stm/spawned.ml2
-rw-r--r--stm/spawned.mli2
-rw-r--r--stm/stm.ml56
-rw-r--r--stm/stm.mli2
-rw-r--r--stm/tQueue.ml2
-rw-r--r--stm/tQueue.mli2
-rw-r--r--stm/tacworkertop.ml2
-rw-r--r--stm/vcs.ml2
-rw-r--r--stm/vcs.mli2
-rw-r--r--stm/vernac_classifier.ml16
-rw-r--r--stm/vernac_classifier.mli2
-rw-r--r--stm/vio_checking.ml2
-rw-r--r--stm/vio_checking.mli2
-rw-r--r--stm/workerLoop.ml2
-rw-r--r--stm/workerLoop.mli2
-rw-r--r--stm/workerPool.ml2
-rw-r--r--stm/workerPool.mli2
27 files changed, 61 insertions, 61 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 3fa1732a4d..25f9d7c187 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 f140f8ed57..a80918e933 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 20d5152aac..6d6a198c5f 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 548958140e..70d4173ae8 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 99e7c92648..bdd71c50bd 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 e783cd8ee1..049286df31 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 8162fc3bb5..a4b35ad60f 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 a55032a470..e23a1d1c18 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 0d2f9cb747..95012d984e 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index 9d30473739..85f0e6bfc1 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 de19dd5352..6ab096abf9 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 acad49f379..c3cf4d67b0 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 a79bf54267..7c96208546 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -476,7 +476,7 @@ end = struct (* {{{ *)
let mk_branch_name { expr = x } = Branch.make
(let rec aux x = match x with
| VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
- | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
| VernacTime (_, e)
| VernacTimeout (_, e) -> aux e
| _ -> "branch" in aux x)
@@ -931,7 +931,7 @@ let show_script ?proof () =
try
let prf =
try match proof with
- | None -> Some (Pfedit.get_current_proof_name ())
+ | None -> Some (Proof_global.get_current_proof_name ())
| Some (p,_) -> Some (p.Proof_global.id)
with Proof_global.NoCurrentProof -> None
in
@@ -1576,8 +1576,10 @@ end = struct (* {{{ *)
let uc =
Option.get
(Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+ (** We only manipulate monomorphic terms here. *)
+ let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
let pr =
- Future.from_val (Option.get (Global.body_of_constant_body c)) in
+ Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
let uc =
Future.chain
~pure:true uc Univ.hcons_universe_context_set in
@@ -1672,7 +1674,7 @@ end (* }}} *)
and TacTask : sig
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
type task = {
t_state : Stateid.t;
t_state_fb : Stateid.t;
@@ -1681,13 +1683,12 @@ and TacTask : sig
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
- exception NoProgress
include AsyncTaskQueue.Task with type task := task
end = struct (* {{{ *)
- type output = Constr.constr * Evd.evar_universe_context
+ type output = (Constr.constr * Evd.evar_universe_context) option
let forward_feedback msg = Hooks.(call forward_feedback msg)
@@ -1709,10 +1710,9 @@ end = struct (* {{{ *)
r_name : string }
type response =
- | RespBuiltSubProof of output
+ | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context)
| RespError of Pp.std_ppcmds
| RespNoProgress
- exception NoProgress
let name = ref "tacworker"
let extra_env () = [||]
@@ -1734,10 +1734,9 @@ end = struct (* {{{ *)
let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
match resp with
- | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+ | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
| RespNoProgress ->
- let e = (NoProgress, Exninfo.null) in
- t_assign (`Exn e);
+ t_assign (`Val None);
t_kill ();
`Stay ((),[])
| RespError msg ->
@@ -1848,8 +1847,8 @@ end = struct (* {{{ *)
else tclUNIT ()
else
let open Notations in
- try
- let pt, uc = Future.join f in
+ match Future.join f with
+ | Some (pt, uc) ->
stm_pperr_endline (fun () -> hov 0 (
str"g=" ++ int (Evar.repr gid) ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
@@ -1857,7 +1856,7 @@ end = struct (* {{{ *)
(if abstract then Tactics.tclABSTRACT None else (fun x -> x))
(V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
Tactics.exact_no_check (EConstr.of_constr pt))
- with TacTask.NoProgress ->
+ | None ->
if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
end)
in
@@ -2046,7 +2045,8 @@ let collect_proof keep cur hd brkind id =
| `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
match cur, (VCS.visit id).step, brkind with
- | (parent, { expr = VernacExactProof _ }), `Fork _, _ ->
+ | (parent, { expr = VernacExactProof _ }), `Fork _, _
+ | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
`Sync (no_name,None,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
| _ ->
@@ -2519,23 +2519,27 @@ let process_transaction ?(newtip=Stateid.fresh ())
anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
(* Query *)
- | VtQuery (false,(report_id,route)), VtNow ->
- (try stm_vernac_interp report_id ~route x
- with e ->
- let e = CErrors.push e in
- Exninfo.iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
- | VtQuery (true,(report_id,_)), w ->
- assert(Stateid.equal report_id Stateid.dummy);
+ | VtQuery (false, route), VtNow ->
+ begin
+ let query_sid = VCS.cur_tip () in
+ try stm_vernac_interp ~route (VCS.cur_tip ()) x
+ with e ->
+ let e = CErrors.push e in
+ Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)
+ end; `Ok
+ (* Part of the script commands don't set the query route *)
+ | VtQuery (true, _route), w ->
let id = VCS.new_node ~id:newtip () in
let queue =
if !Flags.async_proofs_full then `QueryQueue (ref false)
else if Flags.(!compilation_mode = BuildVio) &&
VCS.((get_branch head).kind = `Master) &&
may_pierce_opaque x
- then `SkipQueue
+ then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
Backtrack.record (); if w == VtNow then finish (); `Ok
+
| VtQuery (false,_), VtLater ->
anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
@@ -2765,7 +2769,7 @@ type focus = {
tip : Stateid.t
}
-let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
+let query ~at ~route s =
Future.purify (fun s ->
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
@@ -2778,7 +2782,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
| VtStm (w,_), _ ->
ignore(process_transaction aast (VtStm (w,false), VtNow))
| _ ->
- ignore(process_transaction aast (VtQuery (false,report_with), VtNow)))
+ ignore(process_transaction aast (VtQuery (false, route), VtNow)))
s
let edit_at id =
diff --git a/stm/stm.mli b/stm/stm.mli
index b150f97489..188b176bab 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -34,7 +34,7 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
throwing away side effects except messages. Feedback will
be sent with [report_with], which defaults to the dummy state id *)
val query :
- at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit
+ at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit
(* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if
the requested id is the new document tip hence the document portion following
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index fee4f35b49..56e8c41acd 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 27eca12aff..f005b58ad1 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 256532c6b6..186c8f8b7c 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 df3b8aa621..5d4a812fac 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 46b40f8a4c..6148335676 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 471e05e458..c2ebea961f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -30,9 +30,7 @@ let string_of_vernac_type = function
"ProofStep " ^ string_of_parallel parallel ^
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
- | VtQuery (b,(id,route)) ->
- "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
- " route " ^ string_of_int route
+ | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
| VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b
| VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
@@ -92,8 +90,7 @@ let rec classify_vernac e =
| VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
(* Query *)
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
- | VernacCheckMayEval _ ->
- VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+ | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
(* ProofStep *)
| VernacProof _
| VernacFocus _ | VernacUnfocus
@@ -118,7 +115,7 @@ let rec classify_vernac e =
VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
- | VernacStartTheoremProof (_,l,_) ->
+ | VernacStartTheoremProof (_,l) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
@@ -142,7 +139,7 @@ let rec classify_vernac e =
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
- | VernacInductive (_,_,l) ->
+ | VernacInductive (_, _,_,l) ->
let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
@@ -213,7 +210,6 @@ let rec classify_vernac e =
make_polymorphic res
else res
-let classify_as_query =
- VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
let classify_as_sideeff = VtSideff [], VtLater
let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 45ca5cf6b5..2fa1e0b8dc 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 9f50ab589d..9507e90ba7 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 c0b6d9e6fa..e05f11cb4e 100644
--- a/stm/vio_checking.mli
+++ b/stm/vio_checking.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 86ef59dc30..64121eb3d5 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
index dcbf9c88d6..53f7459357 100644
--- a/stm/workerLoop.mli
+++ b/stm/workerLoop.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 9623765de0..ff4dc5c35e 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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 75c325360e..de396d85b0 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \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-04-30 03:14:33 +0000