diff options
author | 2012-08-20 18:27:02 +0200 | |
---|---|---|
committer | 2012-08-20 18:27:02 +0200 | |
commit | 595aa062e10b8d7100ec2ad9b766f9e624e47295 (patch) | |
tree | 963f9c948173de70209cba5828b372f184afc306 /toplevel | |
parent | ab08ae9f0f944d9f801c44e4ffd3e6b7fcf4b024 (diff) | |
parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) |
Merge tag 'upstream/8.4dfsg' into experimental/master
Upstream version 8.4dfsg
Diffstat (limited to 'toplevel')
56 files changed, 462 insertions, 239 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f4dab15f..3690b924 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 076a946a..1eaf6b76 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 9258a39f..10709abc 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index dd50cda5..3ce8459b 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 24a056d7..912d694e 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,12 +33,18 @@ type info = { nproofs : int; prfname : identifier option; prfdepth : int; + ngoals : int; cmd : vernac_expr; mutable reachable : bool; } let history : info Stack.t = Stack.create () +(** Is this stack active (i.e. nonempty) ? + The stack is currently inactive when compiling files (coqc). *) + +let is_active () = not (Stack.is_empty history) + (** For debug purpose, a dump of the history *) let dump_history () = @@ -74,6 +80,14 @@ let search test = with Found i -> while i != Stack.top history do pop () done +(** An auxiliary function to retrieve the number of remaining subgoals *) + +let get_ngoals () = + try + let prf = Proof_global.give_me_the_proof () in + List.length (Evd.sig_it (Proof.V82.background_subgoals prf)) + with Proof_global.NoCurrentProof -> 0 + (** Register the end of a command and store the current state *) let mark_command ast = @@ -85,6 +99,7 @@ let mark_command ast = prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None); prfdepth = max 0 (Pfedit.current_proof_depth ()); reachable = true; + ngoals = get_ngoals (); cmd = ast } history @@ -175,6 +190,7 @@ let reset_initial () = nproofs = 0; prfname = None; prfdepth = 0; + ngoals = 0; reachable = true; cmd = VernacNop } history @@ -215,10 +231,10 @@ let get_script prf = | _ -> () in (try Stack.iter select history with Not_found -> ()); - (* Get rid of intermediate commands which don't grow the depth *) + (* Get rid of intermediate commands which don't grow the proof depth *) let rec filter n = function | [] -> [] - | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l + | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l | {prfdepth=d}::l -> filter d l in (* initial proof depth (after entering the lemma statement) is 1 *) diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli index 3fde5b11..413ecd2e 100644 --- a/toplevel/backtrack.mli +++ b/toplevel/backtrack.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,6 +19,11 @@ val mark_command : Vernacexpr.vernac_expr -> unit +(** Is this history stack active (i.e. nonempty) ? + The stack is currently inactive when compiling files (coqc). *) + +val is_active : unit -> bool + (** The [Invalid] exception is raised when one of the following function tries to empty the history stack, or reach an unknown states, etc. The stack is preserved in these cases. *) @@ -76,7 +81,7 @@ val mark_unreachable : ?after:int -> Names.identifier list -> unit (** Parse the history stack for printing the script of a proof *) -val get_script : Names.identifier -> Vernacexpr.vernac_expr list +val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list (** For debug purpose, a dump of the history *) @@ -86,6 +91,7 @@ type info = { nproofs : int; prfname : Names.identifier option; prfdepth : int; + ngoals : int; cmd : Vernacexpr.vernac_expr; mutable reachable : bool; } diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 5f2c3dbb..3b6f0f7c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index da9d3590..96c73eb6 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/class.ml b/toplevel/class.ml index c328cc91..52d507a1 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/class.mli b/toplevel/class.mli index 2cc8c453..2228143b 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 18f12582..6914b8f0 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 68a93a74..a61f4f65 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/command.ml b/toplevel/command.ml index dfb1a1b5..8bbe9454 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -294,17 +294,14 @@ let interp_mutual_inductive (paramsl,indl) notations finite = mind_entry_inds = entries }, impls -let eq_constr_expr c1 c2 = - try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false - (* Very syntactical equality *) let eq_local_binder d1 d2 = match d1,d2 with | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) -> List.length nal1 = List.length nal2 && k1 = k2 && List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 && - eq_constr_expr c1 c2 + Constrextern.is_same_type c1 c2 | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) -> - id1 = id2 && eq_constr_expr c1 c2 + id1 = id2 && Constrextern.is_same_type c1 c2 | _ -> false diff --git a/toplevel/command.mli b/toplevel/command.mli index 8ffdbdec..b1cf2053 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e4cfcb3f..66a9516a 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -135,3 +135,11 @@ let init_ocaml_path () = [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] + +let get_compat_version = function + | "8.3" -> Flags.V8_3 + | "8.2" -> Flags.V8_2 + | ("8.1" | "8.0") as s -> + warning ("Compatibility with version "^s^" not supported."); + Flags.V8_2 + | s -> Util.error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 43b1556d..9ca1deb4 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -22,3 +22,5 @@ val init_load_path : unit -> unit val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit + +val get_compat_version : string -> Flags.compat_version diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a60e0d82..df388d1d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,13 +119,6 @@ let compile_files () = Vernac.compile v f) (List.rev !compile_list) -let set_compat_version = function - | "8.3" -> compat_version := Some V8_3 - | "8.2" -> compat_version := Some V8_2 - | "8.1" -> warning "Compatibility with version 8.1 not supported." - | "8.0" -> warning "Compatibility with version 8.0 not supported." - | s -> error ("Unknown compatibility version \""^s^"\".") - (*s options for the virtual machine *) let boxed_val = ref false @@ -152,6 +145,9 @@ let warning s = msg_warning (str s) let ide_slave = ref false let filter_opts = ref false +let verb_compat_ntn = ref false +let no_compat_ntn = ref false + let parse_args arglist = let glob_opt = ref false in let rec parse = function @@ -243,9 +239,13 @@ let parse_args arglist = | "-debug" :: rem -> set_debug (); parse rem - | "-compat" :: v :: rem -> set_compat_version v; parse rem + | "-compat" :: v :: rem -> + Flags.compat_version := get_compat_version v; parse rem | "-compat" :: [] -> usage () + | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem + | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); @@ -332,6 +332,9 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + (* Be careful to set these variables after the inputstate *) + Syntax_def.set_verbose_compat_notations !verb_compat_ntn; + Syntax_def.set_compat_notations (not !no_compat_ntn); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 16d2b874..73e21484 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index bab711ea..7d8807ea 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index f94ed6e3..8c64f3ed 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 958e3dcb..e7b5a0f2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -388,15 +388,12 @@ let explain_unsolvability = function strbrk " (several distinct possible instances found)" let explain_typeclass_resolution env evi k = - match k with - | GoalEvar | InternalHole | ImplicitArg _ -> - (match Typeclasses.class_of_constr evi.evar_concl with - | Some c -> - let env = Evd.evar_env evi in - fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env evi.evar_concl ++ - pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env - | None -> mt()) + match Typeclasses.class_of_constr evi.evar_concl with + | Some c -> + let env = Evd.evar_env evi in + fnl () ++ str "Could not find an instance for " ++ + pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env | _ -> mt() let explain_unsolvable_implicit env evi k explain = @@ -698,12 +695,8 @@ let explain_no_instance env (_,id) l = let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false let pr_constraints printenv env evm = - let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in - let evm = fold_undefined - (fun ev evi evm' -> - if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm - in let l = Evd.to_list evm in + assert(l <> []); let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> eq_named_context_val evi.evar_hyps evi'.evar_hyps) l @@ -719,18 +712,23 @@ let pr_constraints printenv env evm = pr_evar_map None evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evarutil.nf_evar_map evd in - let undef = Evd.undefined_evars evm in + let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in + (* Remove goal evars *) + let undef = fold_undefined + (fun ev evi evm' -> + if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm + in match constr with | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ pr_constraints true env undef | Some (ev, k) -> - explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++ - if List.length (Evd.to_list undef) > 1 then - str"With the following constraints:" ++ fnl() ++ - pr_constraints false env (Evd.remove undef ev) - else mt () + explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++ + (let remaining = Evd.remove undef ev in + if Evd.has_undefined remaining then + str"With the following constraints:" ++ fnl() ++ + pr_constraints false env remaining + else mt ()) let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ @@ -995,6 +993,11 @@ let explain_reduction_tactic_error = function let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in + let tacexpr_differ te te' = + (* NB: The following comparison may raise an exception + since a tacexpr may embed a functional part via a TacExtend *) + try te <> te' with Invalid_argument _ -> false + in let pr_call (n,ck) = (match ck with | Proof_type.LtacNotationCall s -> quote (str s) @@ -1006,11 +1009,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (dummy_loc,te))) ++ (match !otac with - | Some te' when (Obj.magic te' <> te) -> - strbrk " (expanded to " ++ quote - (Pptactic.pr_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te'))) - ++ str ")" + | Some te' when tacexpr_differ (Obj.magic te') te -> + strbrk " (expanded to " ++ quote + (Pptactic.pr_tactic (Global.env()) + (Tacexpr.TacAtom (dummy_loc,te'))) + ++ str ")" | _ -> mt ()) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> let filter = diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index a763472b..84d3ec95 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 9ba3d8b4..0df24c7a 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20120511" +let protocol_version = "20120710" (** * Interface of calls to Coq by CoqIde *) @@ -338,13 +338,25 @@ let to_call = function let of_status s = let of_so = of_option of_string in - Element ("status", [], [of_so s.status_path; of_so s.status_proofname]) + let of_sl = of_list of_string in + Element ("status", [], + [ + of_sl s.status_path; + of_so s.status_proofname; + of_sl s.status_allproofs; + of_int s.status_statenum; + of_int s.status_proofnum; + ] + ) let to_status = function -| Element ("status", [], [path; name]) -> +| Element ("status", [], [path; name; prfs; snum; pnum]) -> { - status_path = to_option to_string path; + status_path = to_list to_string path; status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_statenum = to_int snum; + status_proofnum = to_int pnum; } | _ -> raise Marshal_error @@ -370,14 +382,16 @@ let to_goal = function | _ -> raise Marshal_error let of_goals g = + let of_glist = of_list of_goal in let fg = of_list of_goal g.fg_goals in - let bg = of_list of_goal g.bg_goals in + let bg = of_list (of_pair of_glist of_glist) g.bg_goals in Element ("goals", [], [fg; bg]) let to_goals = function | Element ("goals", [], [fg; bg]) -> + let to_glist = to_list to_goal in let fg = to_list to_goal fg in - let bg = to_list to_goal bg in + let bg = to_list (to_pair to_glist to_glist) bg in { fg_goals = fg; bg_goals = bg; } | _ -> raise Marshal_error @@ -495,9 +509,9 @@ let pr_string s = "["^s^"]" let pr_bool b = if b then "true" else "false" let pr_status s = - let path = match s.status_path with - | None -> "no path; " - | Some p -> "path = " ^ p ^ "; " + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" in let name = match s.status_proofname with | None -> "no proof;" @@ -512,7 +526,14 @@ let pr_mkcases l = let pr_goals_aux g = if g.fg_goals = [] then if g.bg_goals = [] then "Proof completed." - else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) + else + let rec pr_focus _ = function + | [] -> assert false + | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) + | (lg, rg) :: l -> + Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l + in + Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else let pr_menu s = s in let pr_goal { goal_hyp = hyps; goal_ccl = goal } = diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index deee50e5..26c6b671 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 93ad052c..681eec0d 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -132,13 +132,13 @@ let hyp_next_tac sigma env (id,_,ast) = ("exact "^id_s),("exact "^id_s^".\n"); ("generalize "^id_s),("generalize "^id_s^".\n"); ("absurd <"^id_s^">"),("absurd "^type_s^".\n") - ] @ (if Hipattern.is_equality_type ast then [ + ] @ [ ("discriminate "^id_s),("discriminate "^id_s^".\n"); ("injection "^id_s),("injection "^id_s^".\n") - ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [ + ] @ [ ("rewrite "^id_s),("rewrite "^id_s^".\n"); ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n") - ] else []) @ [ + ] @ [ ("elim "^id_s), ("elim "^id_s^".\n"); ("inversion "^id_s), ("inversion "^id_s^".\n"); ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n") @@ -150,11 +150,11 @@ let concl_next_tac sigma concl = "intro"; "intros"; "intuition" - ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [ + ] @ [ "reflexivity"; "discriminate"; "symmetry" - ] else []) @ [ + ] @ [ "assumption"; "omega"; "ring"; @@ -180,19 +180,21 @@ let process_goal sigma g = let process_hyp h_env d acc = let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in (string_of_ppcmds (pr_var_decl h_env d)) :: acc in -(* (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *) let hyps = List.rev (Environ.fold_named_context process_hyp env ~init: []) in { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } -(* hyps,(ccl,concl_next_tac sigma g)) *) let goals () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let fg = List.map (process_goal sigma) all_goals in - let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in - let bg = List.map (process_goal sigma) bgoals in + let (goals, zipper, sigma) = Proof.proof pfts in + let fg = List.map (process_goal sigma) goals in + let map_zip (lg, rg) = + let lg = List.map (process_goal sigma) lg in + let rg = List.map (process_goal sigma) rg in + (lg, rg) + in + let bg = List.map map_zip zipper in Some { Interface.fg_goals = fg; Interface.bg_goals = bg; } with Proof_global.NoCurrentProof -> None @@ -231,16 +233,23 @@ let status () = and display the other parts (opened sections and modules) *) let path = let l = Names.repr_dirpath (Lib.cwd ()) in - let l = snd (Util.list_sep_last l) in - if l = [] then None - else Some (Names.string_of_dirpath (Names.make_dirpath l)) + List.rev_map Names.string_of_id l in let proof = - try - Some (Names.string_of_id (Pfedit.get_current_proof_name ())) + try Some (Names.string_of_id (Proof_global.get_current_proof_name ())) with _ -> None in - { Interface.status_path = path; Interface.status_proofname = proof } + let allproofs = + let l = Proof_global.get_all_proof_names () in + List.map Names.string_of_id l + in + { + Interface.status_path = path; + Interface.status_proofname = proof; + Interface.status_allproofs = allproofs; + Interface.status_statenum = Lib.current_command_label (); + Interface.status_proofnum = Pfedit.current_proof_depth (); + } (** This should be elsewhere... *) let search flags = diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli index 13dff280..fb927cf3 100644 --- a/toplevel/ide_slave.mli +++ b/toplevel/ide_slave.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index de3b62f8..9f1a0218 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 96096d47..7032eb46 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 51eddbae..fa6885af 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 87aedc7b..8ce27708 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/interface.mli b/toplevel/interface.mli index f3374ab4..39fb2a0e 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,17 +29,23 @@ type evar = { } type status = { - status_path : string option; + status_path : string list; (** Module path of the current proof *) status_proofname : string option; - (** Current proof name. [None] if no proof is in progress *) + (** Current proof name. [None] if no focussed proof is in progress *) + status_allproofs : string list; + (** List of all pending proofs. Order is not significant *) + status_statenum : int; + (** A unique id describing the state of coqtop *) + status_proofnum : int; + (** An id describing the state of the current proof. *) } type goals = { fg_goals : goal list; (** List of the focussed goals *) - bg_goals : goal list; - (** List of the background goals *) + bg_goals : (goal list * goal list) list; + (** Zipper representing the unfocussed background goals *) } type hint = (string * string) list diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 7704449f..d6ab44c6 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 8b496f82..e48cb210 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 2f98962c..5977591c 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli index a6a95ccf..cec3597a 100644 --- a/toplevel/libtypes.mli +++ b/toplevel/libtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index cdeff601..775a3af4 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -757,7 +757,7 @@ let interp_modifiers modl = | SetAssoc a :: l -> if assoc <> None then error"An associativity is given more than once."; interp (Some a) level etyps format l - | SetOnlyParsing :: l -> + | SetOnlyParsing _ :: l -> onlyparsing := true; interp assoc level etyps format l | SetFormat s :: l -> @@ -770,8 +770,13 @@ let check_infix_modifiers modifiers = if t <> [] then error "Explicit entry level or type unexpected in infix notation." -let no_syntax_modifiers modifiers = - modifiers = [] or modifiers = [SetOnlyParsing] +let no_syntax_modifiers = function + | [] | [SetOnlyParsing _] -> true + | _ -> false + +let is_only_parsing = function + | [SetOnlyParsing _] -> true + | _ -> false (* Compute precedences from modifiers (or find default ones) *) @@ -1118,7 +1123,7 @@ let add_notation local c ((loc,df),modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) - let onlyparse = modifiers=[SetOnlyParsing] in + let onlyparse = is_only_parsing modifiers in try add_notation_interpretation_core local df c sc onlyparse with NoSyntaxRule -> (* Try to determine a default syntax rule *) @@ -1193,6 +1198,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse = let vars,pat = interp_aconstr i_vars [] c in List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat in - let onlyparse = onlyparse or is_not_printable pat in + let onlyparse = match onlyparse with + | None when (is_not_printable pat) -> Some Flags.Current + | p -> p + in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 32568854..38a0ae59 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -54,7 +54,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : identifier -> identifier list * constr_expr -> - bool -> bool -> unit + bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 025c972f..2059ca60 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -221,11 +221,6 @@ let file_of_name name = * (linked or loaded with load_object). It is used not to load a * module twice. It is NOT the list of ML modules Coq knows. *) -type ml_module_object = { - mlocal : Vernacexpr.locality_flag; - mnames : string list -} - let known_loaded_modules = ref Stringset.empty let add_known_module mname = @@ -235,8 +230,20 @@ let add_known_module mname = let module_is_known mname = Stringset.mem (String.capitalize mname) !known_loaded_modules +(** A plugin is just an ML module with an initialization function. *) + let known_loaded_plugins = ref Stringmap.empty +let add_known_plugin init name = + let name = String.capitalize name in + add_known_module name; + known_loaded_plugins := Stringmap.add name init !known_loaded_plugins + +let init_known_plugins () = + Stringmap.iter (fun _ f -> f()) !known_loaded_plugins + +(** ml object = ml module or plugin *) + let init_ml_object mname = try Stringmap.find mname !known_loaded_plugins () with Not_found -> () @@ -246,81 +253,75 @@ let load_ml_object mname fname= add_known_module mname; init_ml_object mname -let add_known_plugin init name = - let name = String.capitalize name in - add_known_module name; - known_loaded_plugins := Stringmap.add name init !known_loaded_plugins - -let init_known_plugins () = - Stringmap.iter (fun _ f -> f()) !known_loaded_plugins - (* Summary of declared ML Modules *) -(* List and not Stringset because order is important *) +(* List and not Stringset because order is important: most recent first. *) + let loaded_modules = ref [] -let get_loaded_modules () = !loaded_modules +let get_loaded_modules () = List.rev !loaded_modules let add_loaded_module md = loaded_modules := md :: !loaded_modules +let reset_loaded_modules () = loaded_modules := [] -let orig_loaded_modules = ref !loaded_modules -let init_ml_modules () = loaded_modules := !orig_loaded_modules +let if_verbose_load verb f name fname = + if not verb then f name fname + else + let info = "[Loading ML file "^fname^" ..." in + try + f name fname; + msgnl (str (info^" done]")); + with e -> + msgnl (str (info^" failed]")); + raise e + +(** Load a module for the first time (i.e. dynlink it) + or simulate its reload (i.e. doing nothing except maybe + an initialization function). *) + +let cache_ml_object verb reinit name = + begin + if module_is_known name then + (if reinit then init_ml_object name) + else if not has_dynlink then + error ("Dynamic link not supported (module "^name^")") + else + if_verbose_load (verb && is_verbose ()) + load_ml_object name (file_of_name name) + end; + add_loaded_module name let unfreeze_ml_modules x = - loaded_modules := []; - List.iter - (fun name -> - let mname = mod_of_name name in - if not (module_is_known mname) then - if has_dynlink then - let fname = file_of_name mname in - load_ml_object mname fname - else - errorlabstrm "Mltop.unfreeze_ml_modules" - (str"Loading of ML object file forbidden in a native Coq.") - else init_ml_object mname; - add_loaded_module mname) - x + reset_loaded_modules (); + List.iter (cache_ml_object false false) x let _ = Summary.declare_summary "ML-MODULES" - { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); - Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); - Summary.init_function = (fun () -> init_ml_modules ()) } - -(* Same as restore_ml_modules, but verbosely *) - -let cache_ml_module_object (_,{mnames=mnames}) = - List.iter - (fun name -> - let mname = mod_of_name name in - if not (module_is_known mname) then - if has_dynlink then - let fname = file_of_name mname in - try - if_verbose - msg (str"[Loading ML file " ++ str fname ++ str" ..."); - load_ml_object mname fname; - if_verbose msgnl (str" done]"); - add_loaded_module mname - with e -> - if_verbose msgnl (str" failed]"); - raise e - else - (if_verbose msgnl (str" failed]"); - error ("Dynamic link not supported (module "^name^")")) - else init_ml_object mname) - mnames - -let classify_ml_module_object ({mlocal=mlocal} as o) = + { Summary.freeze_function = get_loaded_modules; + Summary.unfreeze_function = unfreeze_ml_modules; + Summary.init_function = reset_loaded_modules } + +(* Liboject entries of declared ML Modules *) + +type ml_module_object = { + mlocal : Vernacexpr.locality_flag; + mnames : string list +} + +let cache_ml_objects (_,{mnames=mnames}) = + List.iter (cache_ml_object true true) mnames + +let classify_ml_objects ({mlocal=mlocal} as o) = if mlocal then Dispose else Substitute o let inMLModule : ml_module_object -> obj = - declare_object {(default_object "ML-MODULE") with - load_function = (fun _ -> cache_ml_module_object); - cache_function = cache_ml_module_object; - subst_function = (fun (_,o) -> o); - classify_function = classify_ml_module_object } + declare_object + {(default_object "ML-MODULE") with + load_function = (fun _ -> cache_ml_objects); + cache_function = cache_ml_objects; + subst_function = (fun (_,o) -> o); + classify_function = classify_ml_objects } let declare_ml_modules local l = + let l = List.map mod_of_name l in Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) let print_ml_path () = @@ -328,7 +329,7 @@ let print_ml_path () = ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++ hv 0 (prlist_with_sep pr_fnl pr_str l)) - (* Printing of loaded ML modules *) +(* Printing of loaded ML modules *) let print_ml_modules () = let l = get_loaded_modules () in diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 99b96ed7..ebea73f1 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -51,27 +51,16 @@ val add_known_module : string -> unit val module_is_known : string -> bool val load_ml_object : string -> string -> unit -(* Declare a plugin and its initialization function. - * A plugin is just an ML module with an initialization function. - * Adding a known plugin implies adding it as a known ML module. - * The initialization function is granted to be called after Coq is fully - * bootstrapped, even if the plugin is statically linked with the toplevel *) +(** Declare a plugin and its initialization function. + A plugin is just an ML module with an initialization function. + Adding a known plugin implies adding it as a known ML module. + The initialization function is granted to be called after Coq is fully + bootstrapped, even if the plugin is statically linked with the toplevel *) val add_known_plugin : (unit -> unit) -> string -> unit -(* Calls all initialization functions in a non-specified order *) +(** Calls all initialization functions in a non-specified order *) val init_known_plugins : unit -> unit -(** Summary of Declared ML Modules *) -val get_loaded_modules : unit -> string list -val add_loaded_module : string -> unit -val init_ml_modules : unit -> unit -val unfreeze_ml_modules : string list -> unit - -type ml_module_object = { - mlocal: Vernacexpr.locality_flag; - mnames: string list; -} - val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit val print_ml_path : unit -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 0c55861f..3708c2f7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/record.mli b/toplevel/record.mli index 45670f1f..f4ae7832 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/search.ml b/toplevel/search.ml index 33e8e51d..3e182689 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/search.mli b/toplevel/search.mli index 95827d54..76821e62 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 8514872b..d5321623 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 757aab1a..0af05d02 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8c9b1078..f6505e30 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,6 +32,8 @@ let print_usage_channel co command = \n -nois start with an empty state\ \n -outputstate f write state in file f.coq\ \n -compat X.Y provides compatibility support for Coq version X.Y\ +\n -verbose-compat-notations be warned when using compatibility notations\ +\n -no-compat-notations get an error when using compatibility notations\ \n\ \n -load-ml-object f load ML object file f\ \n -load-ml-source f load ML file f\ diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 0b98f061..45cedf44 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ed20fc60..3314e82c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,6 +26,30 @@ exception DuringCommandInterp of Util.loc * exn exception HasNotFailed +(* When doing Load on a file, two behaviors are possible: + + - either the history stack is grown by only one command, + the "Load" itself. This is mandatory for command-counting + interfaces (CoqIDE). + + - either each individual sub-commands in the file is added + to the history stack. This allows commands like Show Script + to work across the loaded file boundary (cf. bug #2820). + + The best of the two could probably be combined someday, + in the meanwhile we use a flag. *) + +let atomic_load = ref true + +let _ = + Goptions.declare_bool_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "atomic registration of commands in a Load"; + Goptions.optkey = ["Atomic";"Load"]; + Goptions.optread = (fun () -> !atomic_load); + Goptions.optwrite = ((:=) atomic_load) } + (* Specifies which file is read. The intermediate file names are discarded here. The Drop exception becomes an error. We forget if the error ocurred during interpretation or not *) @@ -272,16 +296,24 @@ and read_vernac_file verbosely s = else Flags.silently Vernacentries.interp in let checknav loc cmd = - if is_navigation_vernac cmd then + if is_navigation_vernac cmd && not (is_reset cmd) then user_error loc "Navigation commands forbidden in files" in + let end_inner_command cmd = + if !atomic_load || is_reset cmd then + Lib.mark_end_of_command () (* for Reset in coqc or coqtop -l *) + else + Backtrack.mark_command cmd; (* for Show Script, cf bug #2820 *) + in let (in_chan, fname, input) = open_file_twice_if verbosely s in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - vernac_com interpfun checknav (parse_sentence input); + let loc_ast = parse_sentence input in + vernac_com interpfun checknav loc_ast; + end_inner_command (snd loc_ast); pp_flush () done with e -> (* whatever the exception *) @@ -324,6 +356,7 @@ let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; try + Lib.mark_end_of_command (); (* in case we're still in coqtop init *) read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; with e -> diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index bcfe9b71..96bc8865 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2324e3e9..fe6bf7db 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -72,10 +72,59 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () +(* indentation code for Show Script, initially contributed + by D. de Rauglaudre *) + +let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = + (* ng1 : number of goals remaining at the current level (before cmd) + ngl1 : stack of previous levels with their remaining goals + ng : number of goals after the execution of cmd + beginend : special indentation stack for { } *) + let ngprev = List.fold_left (+) ng1 ngl1 in + let new_ngl = + if ng > ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let _ = assert (ng = ngprev - 1) in + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) + let show_script () = let prf = Pfedit.get_current_proof_name () in let cmds = Backtrack.get_script prf in - msgnl (Util.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds) + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msgnl (v 0 (Util.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) let show_thesis () = msgnl (anomaly "TODO" ) @@ -311,6 +360,11 @@ let smart_global r = Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; gr +let dump_global r = + try + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr + with _ -> () (**********) (* Syntax *) @@ -389,8 +443,10 @@ let vernac_end_proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - by (Tactics.exact_proof c); - save_named true + let prf = Pfedit.get_current_proof_name () in + by (Tactics.exact_proof c); + save_named true; + Backtrack.mark_unreachable [prf] let vernac_assumption kind l nl= let global = fst kind = Global in @@ -458,9 +514,21 @@ let vernac_cofixpoint l = List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_cofixpoint l -let vernac_scheme = Indschemes.do_scheme - -let vernac_combined_scheme = Indschemes.do_combined_scheme +let vernac_scheme l = + if Dumpglob.dump () then + List.iter (fun (lid, s) -> + Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid; + match s with + | InductionScheme (_, r, _) + | CaseScheme (_, r, _) + | EqualityScheme r -> dump_global r) l; + Indschemes.do_scheme l + +let vernac_combined_scheme lid l = + if Dumpglob.dump () then + (Dumpglob.dump_definition lid false "def"; + List.iter (fun lid -> dump_global (Genarg.AN (Ident lid))) l); + Indschemes.do_combined_scheme lid l (**********************) (* Modules *) @@ -1190,6 +1258,7 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> + Tacinterp.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None @@ -1248,8 +1317,10 @@ let vernac_print = function pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) - | PrintAbout qid -> msg (print_about qid) - | PrintImplicit qid -> msg (print_impargs qid) + | PrintAbout qid -> + msg (print_about qid) + | PrintImplicit qid -> + dump_global qid; msg (print_impargs qid) | PrintAssumptions (o,r) -> (* Prints all the axioms and section variables used by a term *) let cstr = constr_of_global (smart_global r) in @@ -1340,10 +1411,43 @@ let vernac_back n = with Backtrack.Invalid -> error "Invalid backtrack." let vernac_reset_name id = - try Backtrack.reset_name id; try_print_subgoals () - with Backtrack.Invalid -> error "Invalid Reset." + try + let globalized = + try + let gr = Smartlocate.global_with_alias (Ident id) in + Dumpglob.add_glob (fst id) gr; + true + with _ -> false in + + if not globalized then begin + try begin match Lib.find_opening_node (snd id) with + | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id) + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; + (* Might be nice to implement module cases, too.... *) + | _ -> () + end with UserError _ -> () + end; -let vernac_reset_initial () = Backtrack.reset_initial () + if Backtrack.is_active () then + (Backtrack.reset_name id; try_print_subgoals ()) + else + (* When compiling files, Reset is now allowed again + as asked by A. Chlipala. we emulate a simple reset, + that discards all proofs. *) + let lbl = Lib.label_before_name id in + Pfedit.delete_all_proofs (); + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label lbl + with Backtrack.Invalid | Not_found -> error "Invalid Reset." + + +let vernac_reset_initial () = + if Backtrack.is_active () then + Backtrack.reset_initial () + else begin + Pp.msg_warning (str "Reset command occurred in non-interactive mode."); + Lib.reset_label Lib.first_command_label + end (* For compatibility with ProofGeneral: *) @@ -1393,7 +1497,10 @@ let vernac_undoto n = let vernac_focus gln = let p = Proof_global.give_me_the_proof () in let n = match gln with None -> 1 | Some n -> n in - Proof.focus focus_command_cond () n p; print_subgoals () + if n = 0 then + Util.error "Invalid goal number: 0. Goal numbering starts with 1." + else + Proof.focus focus_command_cond () n p; print_subgoals () (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = @@ -1594,11 +1701,11 @@ let interp c = match c with | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> print_subgoals () + | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals () + | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals () | VernacProof (Some tac, Some l) -> - vernac_set_end_tac tac; vernac_set_used_variables l + vernac_set_end_tac tac; vernac_set_used_variables l ; print_subgoals () | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) | VernacToplevelControl e -> raise e diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index a9d384ea..b0d41b15 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,6 +12,8 @@ open Vernacinterp open Vernacexpr open Topconstr +val dump_global : Libnames.reference Genarg.or_by_notation -> unit + (** Vernacular entries *) val show_script : unit -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d9f15337..3106e866 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -128,9 +128,12 @@ type instance_flag = bool option (* Some true = Backward instance; Some false = type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = Decl_kinds.recursivity_kind -type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) +type onlyparsing_flag = Flags.compat_version option + (* Some v = Parse only; None = Print also. + If v<>Current, it contains the name of the coq version + which this notation is trying to be compatible with *) type option_value = Goptionstyp.option_value = | BoolValue of bool @@ -189,7 +192,7 @@ type syntax_modifier = | SetLevel of int | SetAssoc of gram_assoc | SetEntryType of string * simple_constr_prod_entry_key - | SetOnlyParsing + | SetOnlyParsing of Flags.compat_version | SetFormat of string located type proof_end = @@ -377,13 +380,20 @@ let rec is_navigation_vernac = function | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true + | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *) | c -> is_deep_navigation_vernac c and is_deep_navigation_vernac = function - | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l | _ -> false +(* NB: Reset is now allowed again as asked by A. Chlipala *) + +let is_reset = function + | VernacResetInitial | VernacResetName _ -> true + | _ -> false + (* Locating errors raised just after the dot is parsed but before the interpretation phase *) diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 10c5a00f..c4cc4ae5 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 5fdc2b2c..efe7e073 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index aa38e9e9..f90cae73 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index b0fb5491..fed8332b 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |