aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL.doc4
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--tactics/tactics.ml33
-rw-r--r--test-suite/bugs/closed/4273.v9
-rw-r--r--test-suite/complexity/f_equal.v14
-rw-r--r--tools/coqdep.ml37
-rw-r--r--tools/coqdep_boot.ml49
-rw-r--r--tools/coqdep_common.ml39
-rw-r--r--tools/coqdep_common.mli23
9 files changed, 170 insertions, 42 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
index 765880058..2472d2b2a 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -22,8 +22,8 @@ To produce all the documents, the following tools are needed:
- dvips
- bibtex
- makeindex
- - fig2dev
- - convert
+ - fig2dev (transfig)
+ - convert (ImageMagick)
- hevea
- hacha
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8c15f54af..14e334907 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -501,9 +501,9 @@ let f_equal =
let concl = Proofview.Goal.concl gl in
let cut_eq c1 c2 =
try (* type_of can raise an exception *)
- Tacticals.New.tclTHEN
+ Tacticals.New.tclTHENS
(mk_eq _eq c1 c2 Tactics.cut)
- (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))
+ [Proofview.tclUNIT ();Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)]
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bb97c80be..5f7fcce57 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2873,6 +2873,15 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
s'embêter à regarder si un letin_tac ne fait pas des
substitutions aussi sur l'argument voisin *)
+let expand_projections env sigma c =
+ let sigma = Sigma.to_evar_map sigma in
+ let rec aux env c =
+ match kind_of_term c with
+ | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
+ | _ -> map_constr_with_full_binders push_rel aux env c
+ in aux env c
+
+
(* Marche pas... faut prendre en compte l'occurrence précise... *)
let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
@@ -2881,11 +2890,14 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in
let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
let typ0 = reduce_to_quantified_ref indref tmptyp0 in
- let prods, indtyp = decompose_prod typ0 in
+ let prods, indtyp = decompose_prod_assum typ0 in
let hd,argl = decompose_app indtyp in
+ let env' = push_rel_context prods env in
+ let sigma = Proofview.Goal.sigma gl in
let params = List.firstn nparams argl in
+ let params' = List.map (expand_projections env' sigma) params in
(* le gl est important pour ne pas préévaluer *)
- let rec atomize_one i args avoid =
+ let rec atomize_one i args args' avoid =
if Int.equal i nparams then
let t = applist (hd, params@args) in
Tacticals.New.tclTHEN
@@ -2894,22 +2906,23 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
else
let c = List.nth argl (i-1) in
match kind_of_term c with
- | Var id when not (List.exists (occur_var env id) args) &&
- not (List.exists (occur_var env id) params) ->
+ | Var id when not (List.exists (occur_var env id) args') &&
+ not (List.exists (occur_var env id) params') ->
(* Based on the knowledge given by the user, all
constraints on the variable are generalizable in the
current environment so that it is clearable after destruction *)
- atomize_one (i-1) (c::args) (id::avoid)
+ atomize_one (i-1) (c::args) (c::args') (id::avoid)
| _ ->
- if List.exists (dependent c) params ||
- List.exists (dependent c) args
+ let c' = expand_projections env' sigma c in
+ if List.exists (dependent c) params' ||
+ List.exists (dependent c) args'
then
(* This is a case where the argument is constrained in a
way which would require some kind of inversion; we
follow the (old) discipline of not generalizing over
this term, since we don't try to invert the
constraint anyway. *)
- atomize_one (i-1) (c::args) avoid
+ atomize_one (i-1) (c::args) (c'::args') avoid
else
(* We reason blindly on the term and do as if it were
generalizable, ignoring the constraints coming from
@@ -2922,9 +2935,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
let x = fresh_id_in_env avoid id env in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
- (atomize_one (i-1) (mkVar x::args) (x::avoid))
+ (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid))
in
- atomize_one (List.length argl) [] []
+ atomize_one (List.length argl) [] [] []
end }
(* [cook_sign] builds the lists [beforetoclear] (preceding the
diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v
new file mode 100644
index 000000000..591ea4b5b
--- /dev/null
+++ b/test-suite/bugs/closed/4273.v
@@ -0,0 +1,9 @@
+
+
+Set Primitive Projections.
+Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }.
+Theorem onefiber' (q : total2 (fun y => y = 0)) : True.
+Proof. assert (foo:=pr2 _ q). simpl in foo.
+ destruct foo. (* Error: q is used in conclusion. *) exact I. Qed.
+
+Print onefiber'. \ No newline at end of file
diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v
new file mode 100644
index 000000000..86698fa87
--- /dev/null
+++ b/test-suite/complexity/f_equal.v
@@ -0,0 +1,14 @@
+(* Checks that f_equal does not reduce the term uselessly *)
+(* Expected time < 1.00s *)
+
+Fixpoint stupid (n : nat) : unit :=
+match n with
+| 0 => tt
+| S n =>
+ let () := stupid n in
+ let () := stupid n in
+ tt
+end.
+
+Goal stupid 23 = stupid 23.
+Timeout 5 Time f_equal.
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index be50b0e1c..aacfccfd7 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -427,8 +427,9 @@ let coq_dependencies_dump chan dumpboxes =
end
let usage () =
- eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n";
+ eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-Q dir coqdir] [-R dir coqdir] <filename>+\n";
eprintf " extra options:\n";
+ eprintf " -sort : output the file names ordered by dependencies\n";
eprintf " -coqlib dir : set the coq standard library directory\n";
eprintf " -exclude-dir f : skip subdirectories named 'f' during -R search\n";
eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n";
@@ -443,16 +444,17 @@ let rec parse = function
| "-boot" :: ll -> option_boot := true; parse ll
| "-sort" :: ll -> option_sort := true; parse ll
| ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
- | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [];
- add_dir add_known r (split_period ln);
- parse ll
+ | "-I" :: r :: "-as" :: ln :: ll ->
+ add_rec_dir_no_import add_known r [];
+ add_rec_dir_no_import add_known r (split_period ln);
+ parse ll
| "-I" :: r :: "-as" :: [] -> usage ()
| "-I" :: r :: ll -> add_caml_dir r; parse ll
| "-I" :: [] -> usage ()
- | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
+ | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
| "-R" :: r :: "-as" :: [] -> usage ()
- | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll
- | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll
+ | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
+ | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll
| "-R" :: ([] | [_]) -> usage ()
| "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
| "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
@@ -472,24 +474,27 @@ let rec parse = function
let coqdep () =
if Array.length Sys.argv < 2 then usage ();
parse (List.tl (Array.to_list Sys.argv));
+ (* Add current dir with empty logical path if not set by options above. *)
+ (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
+ with Not_found -> add_norec_dir_import add_known "." []);
if not Coq_config.has_natdynlink then option_natdynlk := false;
(* NOTE: These directories are searched from last to first *)
if !option_boot then begin
- add_rec_dir add_known "theories" ["Coq"];
- add_rec_dir add_known "plugins" ["Coq"];
+ add_rec_dir_import add_known "theories" ["Coq"];
+ add_rec_dir_import add_known "plugins" ["Coq"];
add_caml_dir "tactics";
- add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
- add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
+ add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
+ add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
Envars.set_coqlib ~fail:Errors.error;
let coqlib = Envars.coqlib () in
- add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
- add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
+ add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
+ add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
let user = coqlib//"user-contrib" in
- if Sys.file_exists user then add_dir add_coqlib_known user [];
- List.iter (fun s -> add_dir add_coqlib_known s [])
+ if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
+ List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
(Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
- List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath;
+ List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu;
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
new file mode 100644
index 000000000..088ea6bfc
--- /dev/null
+++ b/tools/coqdep_boot.ml
@@ -0,0 +1,49 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Coqdep_common
+
+(** [coqdep_boot] is a stripped-down version of [coqdep], whose
+ behavior is the one of [coqdep -boot]. Its only dependencies
+ are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so.
+ If it needs someday some additional information, pass it via
+ options (see for instance [option_natdynlk] below).
+*)
+
+let rec parse = function
+ | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
+ | "-c" :: ll -> option_c := true; parse ll
+ | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
+ | "-mldep" :: ocamldep :: ll ->
+ option_mldep := Some ocamldep; option_c := true; parse ll
+ | "-I" :: r :: ll ->
+ (* To solve conflict (e.g. same filename in kernel and checker)
+ we allow to state an explicit order *)
+ add_caml_dir r;
+ norec_dirs := StrSet.add r !norec_dirs;
+ parse ll
+ | f :: ll -> treat_file None f; parse ll
+ | [] -> ()
+
+let _ =
+ let () = option_boot := true in
+ if Array.length Sys.argv < 2 then exit 1;
+ parse (List.tl (Array.to_list Sys.argv));
+ if !option_c then begin
+ add_rec_dir_import add_known "." [];
+ add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"];
+ end
+ else begin
+ add_rec_dir_import add_known "theories" ["Coq"];
+ add_rec_dir_import add_known "plugins" ["Coq"];
+ add_caml_dir "tactics";
+ add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
+ add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
+ end;
+ if !option_c then mL_dependencies ();
+ coq_dependencies ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2cdb66aa7..221f3406b 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -210,6 +210,18 @@ let absolute_file_name basename odir =
let dir = match odir with Some dir -> dir | None -> "." in
absolute_dir dir // basename
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+ if it has been given one. Raise [Not_found] otherwise. In
+ particular we can check if "." has been attributed a logical path
+ after processing all options and silently give the default one if
+ it hasn't. We may also use this to warn if ap hysical path is met
+ twice.*)
+let register_dir_logpath,find_dir_logpath =
+ let tbl: (string, string list) Hashtbl.t = Hashtbl.create 19 in
+ let reg physdir logpath = Hashtbl.add tbl (absolute_dir physdir) logpath in
+ let fnd physdir = Hashtbl.find tbl (absolute_dir physdir) in
+ reg,fnd
+
let file_name s = function
| None -> s
| Some "." -> s
@@ -329,7 +341,8 @@ let escape =
Buffer.contents s'
let compare_file f1 f2 =
- absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2)
+ absolute_file_name (Filename.basename f1) (Some (Filename.dirname f1))
+ = absolute_file_name (Filename.basename f2) (Some (Filename.dirname f2))
let canonize f =
let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
@@ -509,11 +522,12 @@ let add_known recur phys_dir log_dir f =
let is_not_seen_directory phys_f =
not (StrSet.mem phys_f !norec_dirs)
-let rec add_directory add_file phys_dir log_dir =
+let rec add_directory recur add_file phys_dir log_dir =
+ register_dir_logpath phys_dir log_dir;
let f = function
| FileDir (phys_f,f) ->
- if is_not_seen_directory phys_f then
- add_directory add_file phys_f (log_dir @ [f])
+ if is_not_seen_directory phys_f && recur then
+ add_directory true add_file phys_f (log_dir @ [f])
| FileRegular f ->
add_file phys_dir log_dir f
in
@@ -523,24 +537,29 @@ let rec add_directory add_file phys_dir log_dir =
else
warning_cannot_open_dir phys_dir
+(** Simply add this directory and imports it, no subdirs. This is used
+ by the implicit adding of the current path (which is not recursive). *)
+let add_norec_dir_import add_file phys_dir log_dir =
+ try add_directory false (add_file true) phys_dir log_dir with Unix_error _ -> ()
+
(** -Q semantic: go in subdirs but only full logical paths are known. *)
-let add_dir add_file phys_dir log_dir =
- try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> ()
+let add_rec_dir_no_import add_file phys_dir log_dir =
+ try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
-let add_rec_dir add_file phys_dir log_dir =
- add_directory (add_file true) phys_dir log_dir
+let add_rec_dir_import add_file phys_dir log_dir =
+ add_directory true (add_file true) phys_dir log_dir
(** -R semantic but only on immediate capitalized subdirs *)
let add_rec_uppercase_subdirs add_file phys_dir log_dir =
process_subdirectories (fun phys_dir f ->
- add_directory (add_file true) phys_dir (log_dir@[String.capitalize f]))
+ add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
phys_dir
(** -I semantic: do not go in subdirs. *)
let add_caml_dir phys_dir =
- add_directory add_caml_known phys_dir []
+ add_directory false add_caml_known phys_dir []
let rec treat_file old_dirname old_name =
let name = Filename.basename old_name
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index c3570f811..0f1c346b3 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -8,6 +8,14 @@
module StrSet : Set.S with type elt = string
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+ if it has been given one. Raise [Not_found] otherwise. In
+ particular we can check if "." has been attributed a logical path
+ after processing all options and silently give the default one if
+ it hasn't. We may also use this to warn if ap hysical path is met
+ twice.*)
+val find_dir_logpath: string -> string list
+
val option_c : bool ref
val option_noglob : bool ref
val option_boot : bool ref
@@ -42,11 +50,22 @@ val add_known : bool -> string -> string list -> string -> unit
val add_coqlib_known : bool -> string -> string list -> string -> unit
val add_caml_known : string -> string list -> string -> unit
val add_caml_dir : string -> unit
-val add_dir :
+
+(** Simply add this directory and imports it, no subdirs. This is used
+ by the implicit adding of the current path. *)
+val add_norec_dir_import :
(bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-val add_rec_dir :
+
+(** -Q semantic: go in subdirs but only full logical paths are known. *)
+val add_rec_dir_no_import :
(bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
+(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
+val add_rec_dir_import :
+ (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
val add_rec_uppercase_subdirs :
(bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
val treat_file : dir -> string -> unit
val error_cannot_parse : string -> int * int -> 'a
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 11:31:32 +0000