aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--config/Makefile.template3
-rw-r--r--config/coq_config.mli2
-rwxr-xr-xconfigure13
-rw-r--r--library/states.ml3
-rw-r--r--parsing/g_vernac.ml421
-rw-r--r--pretyping/pretype_errors.ml19
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--toplevel/coqinit.ml16
-rw-r--r--toplevel/vernacentries.ml30
11 files changed, 62 insertions, 59 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 8194bec77..6ae9ca84a 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -15,6 +15,9 @@
#
#############################################################################
+# Local use (no installation)
+LOCAL=LOCALINSTALLATION
+
# Paths for true installation
# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
# do_Makefile will reside
diff --git a/config/coq_config.mli b/config/coq_config.mli
index cfc3e29cb..4d3258e6a 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -1,6 +1,8 @@
(* $Id$ *)
+val local : bool (* local use (no installation) *)
+
val bindir : string (* where the binaries are installed *)
val coqlib : string (* where the std library is installed *)
diff --git a/configure b/configure
index 8e49f3738..0ca4c98ba 100755
--- a/configure
+++ b/configure
@@ -27,6 +27,7 @@ coq_debug_flag=
coq_profile_flag=
byte_opt_tools=opt
+local=false
bindir_spec=no
libdir_spec=no
mandir_spec=no
@@ -49,8 +50,9 @@ while : ; do
mandir_spec=yes
mandir=$2/man
shift;;
- -local|--local) bindir_spec=yes
- bindir=$COQTOP/bin/${arch-`arch`}
+ -local|--local) local=true
+ bindir_spec=yes
+ bindir=$COQTOP
libdir_spec=yes
libdir=$COQTOP
mandir_spec=yes
@@ -365,7 +367,8 @@ rm -f $COQTOP/config/Makefile
case $ARCH in
win32)
- sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+ sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|`echo $BINDIR |sed -e 's|\\\|/|g'`|" \
-e "s|COQLIBDIRECTORY|`echo $LIBDIR |sed -e 's|\\\|/|g'`|" \
@@ -389,7 +392,8 @@ case $ARCH in
-e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
$COQTOP/config/Makefile.template > $COQTOP/config/Makefile;;
*)
- sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+ sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$BINDIR|" \
-e "s|COQLIBDIRECTORY|$LIBDIR|" \
@@ -423,6 +427,7 @@ rm -f $mlconfig_file
cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
+let local = $local
let bindir = "$BINDIR"
let coqlib = "$LIBDIR"
let coqtop = "$COQTOP"
diff --git a/library/states.ml b/library/states.ml
index be1241a9a..0e60caecb 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,7 +12,8 @@ let get_state () =
let set_state (fl,fs) =
Lib.unfreeze fl;
- unfreeze_summaries fs
+ unfreeze_summaries fs;
+ Lib.declare_initial_state()
let state_magic_number = 19764
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 96b226be4..4fb5380f5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -311,26 +311,23 @@ GEXTEND Gram
END
-(* State management *)
GEXTEND Gram
vernac:
[ [
- IDENT "Save"; IDENT "State"; id = identarg; "." ->
- <:ast< (SaveState $id "") >>
- | IDENT "Save"; IDENT "State"; id = identarg; s = stringarg; "." ->
- <:ast< (SaveState $id $s) >>
- | IDENT "Write"; IDENT "States"; id = identarg; "." ->
- <:ast< (WriteStates $id) >>
- | IDENT "Write"; IDENT "States"; id = stringarg; "." ->
- <:ast< (WriteStates $id) >>
+
+(* State management *)
+ IDENT "Write"; IDENT "State"; id = identarg; "." ->
+ <:ast< (WriteState $id) >>
+ | IDENT "Write"; IDENT "State"; s = stringarg; "." ->
+ <:ast< (WriteState $s) >>
| IDENT "Restore"; IDENT "State"; id = identarg; "." ->
<:ast< (RestoreState $id) >>
- | IDENT "Remove"; IDENT "State"; id = identarg; "." ->
- <:ast< (RemoveState $id) >>
+ | IDENT "Restore"; IDENT "State"; s = stringarg; "." ->
+ <:ast< (RestoreState $s) >>
+ | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
| IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
| IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
<:ast< (ResetSection $id) >>
- | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
(* Modules and Sections *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index a88eeb7e2..4067d0064 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -7,40 +7,41 @@ open Environ
open Type_errors
open Rawterm
-exception PretypeError of loc * path_kind * context * type_error
+let raise_pretype_error (loc,k,ctx,te) =
+ raise (Stdpp.Exc_located (loc, TypeError(k,ctx,te)))
let error_var_not_found_loc loc k s =
- raise (PretypeError (loc,k, Global.context() (*bidon*), VarNotFound s))
+ raise_pretype_error (loc,k, Global.context() (*bidon*), VarNotFound s)
let error_cant_find_case_type_loc loc env expr =
- raise (PretypeError (loc,CCI,context env,CantFindCaseType expr))
+ raise_pretype_error (loc,CCI,context env,CantFindCaseType expr)
let error_ill_formed_branch k env c i actty expty =
raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
let error_number_branches_loc loc k env c ct expn =
- raise (PretypeError (loc, k, context env, NumberBranches (c,ct,expn)))
+ raise_pretype_error (loc, k, context env, NumberBranches (c,ct,expn))
let error_case_not_inductive_loc loc k env c ct =
- raise (PretypeError (loc, k, context env, CaseNotInductive (c,ct)))
+ raise_pretype_error (loc, k, context env, CaseNotInductive (c,ct))
(* Pattern-matching errors *)
let error_bad_constructor_loc loc k cstr ind =
- raise (PretypeError (loc, k, Global.context(), BadConstructor (cstr,ind)))
+ raise_pretype_error (loc, k, Global.context(), BadConstructor (cstr,ind))
let error_wrong_numarg_constructor_loc loc k c n =
- raise (PretypeError (loc, k, Global.context(), WrongNumargConstructor (c,n)))
+ raise_pretype_error (loc, k, Global.context(), WrongNumargConstructor (c,n))
let error_wrong_predicate_arity_loc loc k env c n1 n2 =
- raise (PretypeError (loc, k, context env, WrongPredicateArity (c,n1,n2)))
+ raise_pretype_error (loc, k, context env, WrongPredicateArity (c,n1,n2))
let error_needs_inversion k env x t =
raise (TypeError (k, context env, NeedsInversion (x,t)))
let error_ill_formed_branch_loc loc k env c i actty expty =
- raise (PretypeError (loc, k, context env, IllFormedBranch (c,i,actty,expty)))
+ raise_pretype_error (loc, k, context env, IllFormedBranch (c,i,actty,expty))
let error_occur_check k env ev c =
raise (TypeError (k, context env, OccurCheck (ev,c)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 4671d097d..1292ad75c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -13,8 +13,6 @@ open Rawterm
(* The type of errors raised by the pretyper *)
-exception PretypeError of loc * path_kind * context * type_error
-
val error_var_not_found_loc :
loc -> path_kind -> identifier -> 'a
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6ff3deb70..ab2a0c513 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -228,16 +228,6 @@ let abort_refine f x =
f x
(* used to be: error "Must save or abort current goal first" *)
-let reset_name = abort_refine reset_name
-(*** TODO
-and reset_keeping_name = abort_refine reset_keeping
-and reset_section = abort_refine raw_reset_section
-and save_state = abort_refine States.raw_save_state
-and restore_state = abort_refine States.raw_restore_state
-and restore_last_saved_state = abort_refine States.raw_restore_last_saved_state
-***)
-and reset_initial = abort_refine Lib.reset_initial
-
(*********************************************************************)
(* Modifying the current prooftree *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ab9dc3e43..13f7b6c1c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -51,8 +51,6 @@ val proof_term : unit -> constr
val start_proof : string -> strength -> Coqast.t -> unit
val start_proof_constr : string -> strength -> constr -> unit
-val reset_name : identifier -> unit
-val reset_initial : unit -> unit
val save_named : bool -> unit
val save_anonymous : bool -> string -> 'a -> unit
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 474b247a6..33ee012cf 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -56,19 +56,19 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft
(* Initializes the LoadPath according to COQLIB and Coq_config *)
let init_load_path () =
- (* default load path; only if COQLIB is defined *)
- let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
- let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
- if coqlib = coqtop then
- (* local installation *)
+ if Coq_config.local then
+ (* local use (no installation) *)
List.iter
- (fun s -> add_include (Filename.concat coqtop s))
+ (fun s -> add_include (Filename.concat Coq_config.coqtop s))
("states" :: "dev" ::
(List.map
(fun s -> Filename.concat "theories" (hm2 s))
Coq_config.theories_dirs))
- else
- add_include coqlib;
+ else begin
+ (* default load path; only if COQLIB is defined *)
+ let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
+ add_include coqlib
+ end;
let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
add_include camlp4;
add_include ".";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ce3b0e957..93a330316 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -219,25 +219,38 @@ let _ =
(* Managing states *)
let _ =
- add "SaveState"
+ add "WriteState"
(function
| [VARG_STRING file] ->
- (fun () -> States.extern_state file)
+ (fun () -> Pfedit.abort_refine States.extern_state file)
+ | [VARG_IDENTIFIER id] ->
+ let file = string_of_id id in
+ (fun () -> Pfedit.abort_refine States.extern_state file)
| _ -> bad_vernac_args "SaveState")
let _ =
- add "LoadState"
+ add "RestoreState"
(function
| [VARG_STRING file] ->
- (fun () -> States.intern_state file)
- | _ -> bad_vernac_args "RestoreState")
+ (fun () -> Pfedit.abort_refine States.intern_state file)
+ | [VARG_IDENTIFIER id] ->
+ let file = string_of_id id in
+ (fun () -> Pfedit.abort_refine States.intern_state file)
+ | _ -> bad_vernac_args "LoadState")
(* Resetting *)
let _ =
+ add "ResetName"
+ (function
+ | [VARG_IDENTIFIER id] ->
+ (fun () -> Pfedit.abort_refine Lib.reset_name id)
+ | _ -> bad_vernac_args "ResetName")
+
+let _ =
add "ResetInitial"
(function
- | [] -> (fun () -> reset_initial ())
+ | [] -> (fun () -> Pfedit.abort_refine Lib.reset_initial ())
| _ -> bad_vernac_args "ResetInitial")
(***
@@ -249,11 +262,6 @@ let _ =
| _ -> bad_vernac_args "ResetSection")
***)
-let _ =
- add "ResetName"
- (function
- | [VARG_IDENTIFIER id] -> (fun () -> Pfedit.reset_name id)
- | _ -> bad_vernac_args "ResetName")
(* Modules *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 02:46:15 +0000