aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES6
-rw-r--r--doc/stdlib/index-list.html.template1
-rw-r--r--grammar/tacextend.mlp142
-rw-r--r--grammar/vernacextend.mlp16
-rw-r--r--intf/extend.ml9
-rw-r--r--kernel/inductive.ml3
-rw-r--r--lib/coqProject_file.ml487
-rw-r--r--lib/coqProject_file.mli42
-rw-r--r--lib/genarg.ml13
-rw-r--r--lib/genarg.mli3
-rw-r--r--man/coqdep.13
-rw-r--r--plugins/ltac/g_eqdecide.ml41
-rw-r--r--plugins/ltac/taccoerce.ml76
-rw-r--r--plugins/ltac/taccoerce.mli19
-rw-r--r--plugins/ltac/tacentries.ml135
-rw-r--r--plugins/ltac/tacentries.mli12
-rw-r--r--plugins/ltac/tacinterp.ml98
-rw-r--r--plugins/ltac/tacinterp.mli8
-rw-r--r--plugins/nsatz/g_nsatz.ml41
-rw-r--r--test-suite/failure/fixpointeta.v70
-rw-r--r--theories/Compat/Coq87.v1
-rw-r--r--theories/Compat/Coq88.v11
-rw-r--r--tools/CoqMakefile.in9
-rw-r--r--tools/coq_makefile.ml71
-rw-r--r--tools/coqdep.ml19
-rw-r--r--vernac/himsg.ml2
26 files changed, 553 insertions, 305 deletions
diff --git a/CHANGES b/CHANGES
index 51b812a201..1c7c53f296 100644
--- a/CHANGES
+++ b/CHANGES
@@ -109,6 +109,12 @@ CoqIDE
- Find and Replace All report the number of occurrences found; Find indicates
when it wraps.
+coqdep
+
+- Learned to read -I, -Q, -R and filenames from _CoqProject files.
+ This is used by coq_makefile when generating dependencies for .v
+ files (but not other files).
+
Documentation
- The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a2739e457e..8c09b23a5a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -598,5 +598,6 @@ through the <tt>Require Import</tt> command.</p>
theories/Compat/AdmitAxiom.v
theories/Compat/Coq86.v
theories/Compat/Coq87.v
+ theories/Compat/Coq88.v
</dd>
</dl>
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 6c072e36ad..525be64325 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -13,15 +13,6 @@
open Q_util
open Argextend
-(** Quotation difference for match clauses *)
-
-let default_patt loc =
- (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-let make_fun loc cl =
- let l = cl @ [default_patt loc] in
- MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
let plugin_name = <:expr< __coq_plugin_name >>
let mlexpr_of_ident id =
@@ -29,112 +20,33 @@ let mlexpr_of_ident id =
let id = "$" ^ id in
<:expr< Names.Id.of_string_soft $str:id$ >>
-let rec make_patt = function
- | [] -> <:patt< [] >>
- | ExtNonTerminal (_, Some p) :: l ->
- <:patt< [ $lid:p$ :: $make_patt l$ ] >>
- | _::l -> make_patt l
-
-let rec make_let raw e = function
- | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
- | ExtNonTerminal (g, Some p) :: l ->
- let t = type_of_user_symbol g in
- let loc = MLast.loc_of_expr e in
- let e = make_let raw e l in
- let v =
- if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
- else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
- <:expr< let $lid:p$ = $v$ in $e$ >>
- | _::l -> make_let raw e l
-
-let make_clause (pt,e) =
- (make_patt pt,
- ploc_vala None,
- make_let false e pt)
-
-let make_fun_clauses loc s l =
- let map c = make_fun loc [make_clause c] in
- mlexpr_of_list map l
-
-let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >>
-
let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
| Uentry e ->
- let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
- <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+ let wit = <:expr< $lid:"wit_"^e$ >> in
+ <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
| Uentryl (e, l) ->
assert (e = "tactic");
- let arg = get_argt <:expr< Tacarg.wit_tactic >> in
- <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
-
-let make_prod_item = function
- | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
- | ExtNonTerminal (g, id) ->
- <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >>
-
-let mlexpr_of_clause cl =
- mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl
-
-(** Special treatment of constr entries *)
-let is_constr_gram = function
-| ExtTerminal _ -> false
-| ExtNonTerminal (Uentry "constr", _) -> true
-| _ -> false
-
-let make_var = function
- | ExtNonTerminal (_, p) -> p
- | _ -> assert false
-
-let declare_tactic loc tacname ~level clause = match clause with
-| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem ->
- (** The extension is only made of a name followed by constr entries: we do not
- add any grammar nor printing rule and add it as a true Ltac definition. *)
- let patt = make_patt rem in
- let vars = List.map make_var rem in
- let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
- let entry = mlexpr_of_string tacname in
- let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
- let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
- let name = mlexpr_of_string name in
- let tac = match rem with
- | [] ->
- (** Special handling of tactics without arguments: such tactics do not do
- a Proofview.Goal.nf_enter to compute their arguments. It matters for some
- whole-prof tactics like [shelve_unifiable]. *)
- <:expr< fun _ $lid:"ist"$ -> $tac$ >>
- | _ ->
- let f = make_fun loc [patt, ploc_vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
- <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
- in
- (** Arguments are not passed directly to the ML tactic in the TacML node,
- the ML tactic retrieves its arguments in the [ist] environment instead.
- This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
- let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in
- let name = <:expr< Names.Id.of_string $name$ >> in
- declare_str_items loc
- [ <:str_item< do {
- let obj () = Tacenv.register_ltac True False $name$ $body$ in
- let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in
- Mltop.declare_cache_obj obj $plugin_name$ } >>
- ]
-| _ ->
- (** Otherwise we add parsing and printing rules to generate a call to a
- TacML tactic. *)
- let entry = mlexpr_of_string tacname in
- let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
- let gl = mlexpr_of_clause clause in
- let level = mlexpr_of_int level in
- let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in
- declare_str_items loc
- [ <:str_item< do {
- Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
- Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
- ]
+ let wit = <:expr< $lid:"wit_"^e$ >> in
+ <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
+
+let rec mlexpr_of_clause = function
+| [] -> <:expr< TyNil >>
+| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
+| ExtNonTerminal(g,None) :: cl ->
+ <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >>
+| ExtNonTerminal(g,Some id) :: cl ->
+ <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >>
+
+let rec binders_of_clause e = function
+| [] -> <:expr< fun ist -> $e$ >>
+| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
+| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
+| _ :: cl -> binders_of_clause e cl
open Pcaml
@@ -146,13 +58,17 @@ EXTEND
OPT "|"; l = LIST1 tacrule SEP "|";
"END" ->
let level = match level with Some i -> int_of_string i | None -> 0 in
- declare_tactic loc s ~level l ] ]
+ let level = mlexpr_of_int level in
+ let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
+ declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
;
tacrule:
[ [ "["; l = LIST1 tacargs; "]";
- "->"; "["; e = Pcaml.expr; "]" -> (l,e)
+ "->"; "["; e = Pcaml.expr; "]" ->
+ <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
] ]
;
+
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 24ee0042be..a2872d07f6 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -12,7 +12,6 @@
open Q_util
open Argextend
-open Tacextend
type rule = {
r_head : string option;
@@ -27,6 +26,21 @@ type rule = {
(** Whether this entry is deprecated *)
}
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+ (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
+
+let make_fun loc cl =
+ let l = cl @ [default_patt loc] in
+ MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
+
+let rec make_patt = function
+ | [] -> <:patt< [] >>
+ | ExtNonTerminal (_, Some p) :: l ->
+ <:patt< [ $lid:p$ :: $make_patt l$ ] >>
+ | _::l -> make_patt l
+
let rec make_let e = function
| [] -> e
| ExtNonTerminal (g, Some p) :: l ->
diff --git a/intf/extend.ml b/intf/extend.ml
index 10c9b3dc14..734b859f60 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -85,6 +85,15 @@ type 'a user_symbol =
| Uentry of 'a
| Uentryl of 'a * int
+type ('a,'b,'c) ty_user_symbol =
+| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
+| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
+| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
+
(** {5 Type-safe grammar extension} *)
type ('self, 'a) symbol =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 91c042130a..9bed598bb7 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1069,6 +1069,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
try find_inductive env a
with Not_found ->
raise_err env i (RecursionNotOnInductiveType a) in
+ let mib,_ = lookup_mind_specif env (out_punivs mind) in
+ if mib.mind_finite != Finite then
+ raise_err env i (RecursionNotOnInductiveType a);
(mind, (env', b))
else check_occur env' (n+1) b
else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 40945939f2..d6c340f691 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -8,27 +8,32 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
type project = {
project_file : string option;
makefile : string option;
install_kind : install option;
use_ocamlopt : bool;
- v_files : string list;
- mli_files : string list;
- ml4_files : string list;
- ml_files : string list;
- mllib_files : string list;
- mlpack_files : string list;
-
- ml_includes : path list;
- r_includes : (path * logic_path) list;
- q_includes : (path * logic_path) list;
- extra_args : string list;
- defs : (string * string) list;
-
- extra_targets : extra_target list;
- subdirs : string list;
+ v_files : string sourced list;
+ mli_files : string sourced list;
+ ml4_files : string sourced list;
+ ml_files : string sourced list;
+ mllib_files : string sourced list;
+ mlpack_files : string sourced list;
+
+ ml_includes : path sourced list;
+ r_includes : (path * logic_path) sourced list;
+ q_includes : (path * logic_path) sourced list;
+ extra_args : string sourced list;
+ defs : (string * string) sourced list;
+
+ (* deprecated in favor of a Makefile.local using :: rules *)
+ extra_targets : extra_target sourced list;
+ subdirs : string sourced list;
}
and extra_target = {
target : string;
@@ -114,6 +119,7 @@ let exists_dir dir =
let process_cmd_line orig_dir proj args =
let parsing_project_file = ref (proj.project_file <> None) in
+ let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
let orig_dir = (* avoids turning foo.v in ./foo.v *)
if orig_dir = "." then "" else orig_dir in
let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
@@ -143,17 +149,17 @@ let process_cmd_line orig_dir proj args =
aux { proj with install_kind = Some install } r
| "-extra" :: target :: dependencies :: command :: r ->
let tgt = { target; dependencies; phony = false; command } in
- aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+ aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
| "-extra-phony" :: target :: dependencies :: command :: r ->
let tgt = { target; dependencies; phony = true; command } in
- aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+ aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
| "-Q" :: d :: lp :: r ->
- aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
+ aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r
| "-I" :: d :: r ->
- aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+ aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r
| "-R" :: d :: lp :: r ->
- aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+ aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r
| "-f" :: file :: r ->
if !parsing_project_file then
@@ -178,20 +184,21 @@ let process_cmd_line orig_dir proj args =
error "Option -o given more than once";
aux { proj with makefile = Some file } r
| v :: "=" :: def :: r ->
- aux { proj with defs = proj.defs @ [v,def] } r
+ aux { proj with defs = proj.defs @ [sourced (v,def)] } r
| "-arg" :: a :: r ->
- aux { proj with extra_args = proj.extra_args @ [a] } r
+ aux { proj with extra_args = proj.extra_args @ [sourced a] } r
| f :: r ->
let f = CUnix.correct_path f orig_dir in
let proj =
- if exists_dir f then { proj with subdirs = proj.subdirs @ [f] }
+ if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
else match CUnix.get_extension f with
- | ".v" -> { proj with v_files = proj.v_files @ [f] }
- | ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
- | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] }
- | ".mli" -> { proj with mli_files = proj.mli_files @ [f] }
- | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] }
- | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] }
+ | ".v" ->
+ { proj with v_files = proj.v_files @ [sourced f] }
+ | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
+ | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
+ | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
+ | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
+ | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] }
| _ -> raise (Parsing_error ("Unknown option "^f)) in
aux proj r
in
@@ -215,16 +222,34 @@ let rec find_project_file ~from ~projfile_name =
else find_project_file ~from:newdir ~projfile_name
;;
+let all_files { v_files; ml_files; mli_files; ml4_files;
+ mllib_files; mlpack_files } =
+ v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files
+
+let map_sourced_list f l = List.map (fun x -> f x.thing) l
+;;
+
+let map_cmdline f l = CList.map_filter (function
+ | {thing=x; source=CmdLine} -> Some (f x)
+ | {source=ProjectFile} -> None) l
+
let coqtop_args_from_project
{ ml_includes; r_includes; q_includes; extra_args }
=
- let map = List.map in
+ let map = map_sourced_list in
let args =
map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @
map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @
map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @
- [extra_args] in
+ [map (fun x -> x) extra_args] in
List.flatten args
;;
+let filter_cmdline l = CList.map_filter
+ (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None)
+ l
+;;
+
+let forget_source {thing} = thing
+
(* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 5a4dd3659f..5780bb5d78 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -10,29 +10,32 @@
exception Parsing_error of string
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
type project = {
project_file : string option;
makefile : string option;
install_kind : install option;
use_ocamlopt : bool;
- v_files : string list;
- mli_files : string list;
- ml4_files : string list;
- ml_files : string list;
- mllib_files : string list;
- mlpack_files : string list;
+ v_files : string sourced list;
+ mli_files : string sourced list;
+ ml4_files : string sourced list;
+ ml_files : string sourced list;
+ mllib_files : string sourced list;
+ mlpack_files : string sourced list;
- ml_includes : path list;
- r_includes : (path * logic_path) list;
- q_includes : (path * logic_path) list;
- extra_args : string list;
- defs : (string * string) list;
+ ml_includes : path sourced list;
+ r_includes : (path * logic_path) sourced list;
+ q_includes : (path * logic_path) sourced list;
+ extra_args : string sourced list;
+ defs : (string * string) sourced list;
(* deprecated in favor of a Makefile.local using :: rules *)
- extra_targets : extra_target list;
- subdirs : string list;
-
+ extra_targets : extra_target sourced list;
+ subdirs : string sourced list;
}
and extra_target = {
target : string;
@@ -52,3 +55,14 @@ val read_project_file : string -> project
val coqtop_args_from_project : project -> string list
val find_project_file : from:string -> projfile_name:string -> string option
+val all_files : project -> string sourced list
+
+val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list
+
+(** Only uses the elements with source=CmdLine *)
+val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list
+
+(** Only uses the elements with source=CmdLine *)
+val filter_cmdline : 'a sourced list -> 'a list
+
+val forget_source : 'a sourced -> 'a
diff --git a/lib/genarg.ml b/lib/genarg.ml
index cf3a2bee7f..209d1b271e 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -174,19 +174,22 @@ sig
val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
end
+let get_arg_tag = function
+| ExtraArg s -> s
+| _ -> assert false
+
module Register (M : GenObj) =
struct
module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
let arg0_map = ref GenMap.empty
- let register0 arg f = match arg with
- | ExtraArg s ->
+ let register0 arg f =
+ let s = get_arg_tag arg in
if GenMap.mem s !arg0_map then
let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
CErrors.anomaly msg
else
arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
- | _ -> assert false
let get_obj0 name =
try
@@ -199,8 +202,6 @@ struct
(** For now, the following function is quite dummy and should only be applied
to an extra argument type, otherwise, it will badly fail. *)
- let obj t = match t with
- | ExtraArg s -> get_obj0 s
- | _ -> assert false
+ let obj t = get_obj0 @@ get_arg_tag t
end
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d49cb334a0..bb85f99e3c 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -159,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
This is boilerplate code used here and there in the code of Coq. *)
+val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag
+(** Works only on base objects (ExtraArg), otherwise fails badly. *)
+
module type GenObj =
sig
type ('raw, 'glb, 'top) obj
diff --git a/man/coqdep.1 b/man/coqdep.1
index ed727db7c8..c417402c25 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -80,6 +80,9 @@ Prints the dependencies of Caml modules.
\" of each Coq file given as argument and complete (if needed)
\" the list of Caml modules. The new command is printed on
\" the standard output. No dependency is computed with this option.
+.TP
+.BI \-f \ file
+Read filenames and options -I, -R and -Q from a _CoqProject FILE.
.TP
.BI \-I/\-Q/\-R \ options
Have the same effects on load path and modules names as for other
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index b3bcc99840..2251a66204 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
(************************************************************************)
open Eqdecide
+open Stdarg
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4665ff9ed3..2c7ebb7458 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -16,6 +16,7 @@ open Misctypes
open Genarg
open Stdarg
open Geninterp
+open Pp
exception CannotCoerceTo of string
@@ -94,6 +95,38 @@ let to_option v = prj Val.typ_opt v
let to_pair v = prj Val.typ_pair v
+let cast_error wit v =
+ let pr_v = Pptactic.pr_value Pptactic.ltop v in
+ let Val.Dyn (tag, _) = v in
+ let tag = Val.pr tag in
+ CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+ ++ str " while type " ++ Val.pr wit ++ str " was expected.")
+
+let unbox wit v ans = match ans with
+| None -> cast_error wit v
+| Some x -> x
+
+let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
+| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
+| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
+| Val.Pair (tag1, tag2) ->
+ let (x, y) = unbox Val.typ_pair v (to_pair v) in
+ (prj tag1 x, prj tag2 y)
+| Val.Base t ->
+ let Val.Dyn (t', x) = v in
+ match Val.eq t t' with
+ | None -> cast_error t v
+ | Some Refl -> x
+let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
+| ExtraArg _ -> Geninterp.val_tag (topwit wit)
+| ListArg t -> Val.List (tag_of_arg t)
+| OptArg t -> Val.Opt (tag_of_arg t)
+| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
+
+let val_cast arg v = prj (tag_of_arg arg) v
+
+let cast (Topwit wit) v = val_cast wit v
+
end
let is_variable env id =
@@ -334,3 +367,46 @@ let coerce_to_int_or_var_list v =
| Some l ->
let map n = ArgArg (coerce_to_int n) in
List.map map l
+
+(** Abstract application, to print ltac functions *)
+type appl =
+ | UnnamedAppl (** For generic applications: nothing is printed *)
+ | GlbAppl of (Names.KerName.t * Val.t list) list
+ (** For calls to global constants, some may alias other. *)
+
+(* Values for interpretation *)
+type tacvalue =
+ | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+ Name.t list * Tacexpr.glob_tactic_expr
+ | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
+
+let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
+ let wit = Genarg.create_arg "tacvalue" in
+ let () = register_val0 wit None in
+ let () = Genprint.register_val_print0 (base_val_typ wit)
+ (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
+ wit
+
+let pr_argument_type arg =
+ let Val.Dyn (tag, _) = arg in
+ Val.pr tag
+
+(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
+
+(* Displays a value *)
+let pr_value env v =
+ let pr_with_env pr =
+ match env with
+ | Some (env,sigma) -> pr env sigma
+ | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
+ let open Genprint in
+ match generic_val_print v with
+ | TopPrinterBasic pr -> pr ()
+ | TopPrinterNeedsContext pr -> pr_with_env pr
+ | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+ pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
+
+let error_ltac_variable ?loc id env v s =
+ CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++
+ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
+ strbrk "which cannot be coerced to " ++ str s ++ str".")
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index ce05d70e88..1fa5e3c076 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -42,6 +42,7 @@ sig
val to_list : t -> t list option
val to_option : t -> t option option
val to_pair : t -> (t * t) option
+ val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
end
(** {5 Coercion functions} *)
@@ -92,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type
+
+val error_ltac_variable : ?loc:Loc.t -> Id.t ->
+ (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
+
+(** Abstract application, to print ltac functions *)
+type appl =
+ | UnnamedAppl (** For generic applications: nothing is printed *)
+ | GlbAppl of (Names.KerName.t * Val.t list) list
+ (** For calls to global constants, some may alias other. *)
+
+type tacvalue =
+ | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+ Name.t list * Tacexpr.glob_tactic_expr
+ | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
+
+val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type
+
+val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 42f2abd73c..566fc28733 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -554,3 +554,138 @@ let () =
AnyEntry Pltac.tactic_arg;
] in
register_grammars_by_name "tactic" entries
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+ (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+ ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu ->
+ match tu with
+ | TUlist1 l -> Ulist1(untype_user_symbol l)
+ | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s)
+ | TUlist0 l -> Ulist0(untype_user_symbol l)
+ | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s)
+ | TUopt(o) -> Uopt(untype_user_symbol o)
+ | TUentry a -> Uentry (Genarg.ArgT.Any a)
+ | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i)
+
+let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
+ fun sign -> match sign with
+ | TyNil -> []
+ | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
+ | TyArg ((loc,(a,id)),sig') ->
+ TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
+ | TyAnonArg ((loc,a),sig') ->
+ TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig'
+
+let clause_of_ty_ml = function
+ | TyML (t,_) -> clause_of_sign t
+
+let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
+ | TUentry a -> ExtraArg a
+ | TUentryl (a,l) -> ExtraArg a
+ | TUopt(o) -> OptArg (prj o)
+ | TUlist1 l -> ListArg (prj l)
+ | TUlist1sep (l,_) -> ListArg (prj l)
+ | TUlist0 l -> ListArg (prj l)
+ | TUlist0sep (l,_) -> ListArg (prj l)
+
+let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
+ fun sign tac ->
+ match sign with
+ | TyNil ->
+ begin fun vals ist -> match vals with
+ | [] -> tac ist
+ | _ :: _ -> assert false
+ end
+ | TyIdent (s, sig') -> eval_sign sig' tac
+ | TyArg ((_loc,(a,id)), sig') ->
+ let f = eval_sign sig' in
+ begin fun tac vals ist -> match vals with
+ | [] -> assert false
+ | v :: vals ->
+ let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+ f (tac v') vals ist
+ end tac
+ | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac
+
+let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
+ | TyML (t,tac) -> eval_sign t tac
+
+let is_constr_entry = function
+| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr
+| _ -> false
+
+let rec only_constr : type a. a ty_sig -> bool = function
+| TyNil -> true
+| TyIdent(_,_) -> false
+| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false
+| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false
+
+let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
+| TyNil -> []
+| TyIdent (_,s) -> mk_sign_vars s
+| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s
+| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s
+
+let dummy_id = Id.of_string "_"
+
+let lift_constr_tac_to_ml_tac vars tac =
+ let tac _ ist = Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let map = function
+ | Anonymous -> None
+ | Name id ->
+ let c = Id.Map.find id ist.Geninterp.lfun in
+ try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c)
+ with Taccoerce.CannotCoerceTo ty ->
+ Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty
+ in
+ let args = List.map_filter map vars in
+ tac args ist
+ end in
+ tac
+
+let tactic_extend plugin_name tacname ~level sign =
+ let open Tacexpr in
+ let ml_tactic_name =
+ { mltac_tactic = tacname;
+ mltac_plugin = plugin_name }
+ in
+ match sign with
+ | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
+ (** The extension is only made of a name followed by constr entries: we do not
+ add any grammar nor printing rule and add it as a true Ltac definition. *)
+ (*
+ let patt = make_patt rem in
+ let vars = List.map make_var rem in
+ let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
+ *)
+ let vars = mk_sign_vars s in
+ let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
+ let tac = match s with
+ | TyNil -> eval ml_tac
+ (** Special handling of tactics without arguments: such tactics do not do
+ a Proofview.Goal.nf_enter to compute their arguments. It matters for some
+ whole-prof tactics like [shelve_unifiable]. *)
+ | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac)
+ in
+ (** Arguments are not passed directly to the ML tactic in the TacML node,
+ the ML tactic retrieves its arguments in the [ist] environment instead.
+ This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+ let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
+ let id = Names.Id.of_string name in
+ let obj () = Tacenv.register_ltac true false id body in
+ let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+ Mltop.declare_cache_obj obj plugin_name
+ | _ ->
+ let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+ Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
+ Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 02e2f0f60e..3f804ee8d1 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -67,3 +67,15 @@ val print_ltacs : unit -> unit
val print_located_tactic : Libnames.reference -> unit
(** Display the absolute name of a tactic. *)
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+ (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+ ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index cd9d9bac2c..991afe9c60 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -79,9 +79,6 @@ let out_gen wit v =
let val_tag wit = val_tag (topwit wit)
-let base_val_typ wit =
- match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
-
let pr_argument_type arg =
let Val.Dyn (tag, _) = arg in
Val.pr tag
@@ -93,11 +90,6 @@ let safe_msgnl s =
type value = Val.t
-(** Abstract application, to print ltac functions *)
-type appl =
- | UnnamedAppl (** For generic applications: nothing is printed *)
- | GlbAppl of (Names.KerName.t * Val.t list) list
- (** For calls to global constants, some may alias other. *)
let push_appl appl args =
match appl with
| UnnamedAppl -> UnnamedAppl
@@ -121,19 +113,6 @@ let combine_appl appl1 appl2 =
| UnnamedAppl,a | a,UnnamedAppl -> a
| GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1)
-(* Values for interpretation *)
-type tacvalue =
- | VFun of appl*ltac_trace * value Id.Map.t *
- Name.t list * glob_tactic_expr
- | VRec of value Id.Map.t ref * glob_tactic_expr
-
-let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
- let wit = Genarg.create_arg "tacvalue" in
- let () = register_val0 wit None in
- let () = Genprint.register_val_print0 (base_val_typ wit)
- (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
- wit
-
let of_tacvalue v = in_gen (topwit wit_tacvalue) v
let to_tacvalue v = out_gen (topwit wit_tacvalue) v
@@ -169,39 +148,6 @@ module Value = struct
let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
of_tacvalue closure
- let cast_error wit v =
- let pr_v = Pptactic.pr_value Pptactic.ltop v in
- let Val.Dyn (tag, _) = v in
- let tag = Val.pr tag in
- user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
- ++ str " while type " ++ Val.pr wit ++ str " was expected.")
-
- let unbox wit v ans = match ans with
- | None -> cast_error wit v
- | Some x -> x
-
- let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
- | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
- | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
- | Val.Pair (tag1, tag2) ->
- let (x, y) = unbox Val.typ_pair v (to_pair v) in
- (prj tag1 x, prj tag2 y)
- | Val.Base t ->
- let Val.Dyn (t', x) = v in
- match Val.eq t t' with
- | None -> cast_error t v
- | Some Refl -> x
-
- let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
- | ExtraArg _ -> val_tag wit
- | ListArg t -> Val.List (tag_of_arg t)
- | OptArg t -> Val.Opt (tag_of_arg t)
- | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
-
- let val_cast arg v = prj (tag_of_arg arg) v
-
- let cast (Topwit wit) v = val_cast wit v
-
end
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -233,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
| None -> DebugOff
| Some level -> level
-(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
-
-(* Displays a value *)
-let pr_value env v =
- let pr_with_env pr =
- match env with
- | Some (env,sigma) -> pr env sigma
- | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
- let open Genprint in
- match generic_val_print v with
- | TopPrinterBasic pr -> pr ()
- | TopPrinterNeedsContext pr -> pr_with_env pr
- | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
- pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
-
let pr_closure env ist body =
let pp_body = Pptactic.pr_glob_tactic env body in
let pr_sep () = fnl () in
@@ -360,15 +291,11 @@ let debugging_exception_step ist signal_anomaly e pp =
debugging_step ist (fun () ->
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
-let error_ltac_variable ?loc id env v s =
- user_err ?loc (str "Ltac variable " ++ Id.print id ++
- strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
- strbrk "which cannot be coerced to " ++ str s ++ str".")
-
(* Raise Not_found if not in interpretation sign *)
let try_interp_ltac_var coerce ist env {loc;v=id} =
let v = Id.Map.find id ist.lfun in
- try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
+ try coerce v with CannotCoerceTo s ->
+ Taccoerce.error_ltac_variable ?loc id env v s
let interp_ltac_var coerce ist env locid =
try try_interp_ltac_var coerce ist env locid
@@ -2090,27 +2017,6 @@ let _ =
in
Pretyping.register_constr_interp0 wit_tactic eval
-(** Used in tactic extension **)
-
-let dummy_id = Id.of_string "_"
-
-let lift_constr_tac_to_ml_tac vars tac =
- let tac _ ist = Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = project gl in
- let map = function
- | Anonymous -> None
- | Name id ->
- let c = Id.Map.find id ist.lfun in
- try Some (coerce_to_closed_constr env c)
- with CannotCoerceTo ty ->
- error_ltac_variable dummy_id (Some (env,sigma)) c ty
- in
- let args = List.map_filter map vars in
- tac args ist
- end in
- tac
-
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 3f3b8e5558..bd44bdbea4 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -133,13 +133,5 @@ val interp_int : interp_sign -> lident -> int
val interp_int_or_var : interp_sign -> int or_var -> int
-val error_ltac_variable : ?loc:Loc.t -> Id.t ->
- (Environ.env * Evd.evar_map) option -> value -> string -> 'a
-
-(** Transforms a constr-expecting tactic into a tactic finding its arguments in
- the Ltac environment according to the given names. *)
-val lift_constr_tac_to_ml_tac : Name.t list ->
- (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
-
val default_ist : unit -> Geninterp.interp_sign
(** Empty ist with debug set on the current value. *)
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index c8112eaa99..4ac49adb90 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -9,6 +9,7 @@
(************************************************************************)
open Ltac_plugin
+open Stdarg
DECLARE PLUGIN "nsatz_plugin"
diff --git a/test-suite/failure/fixpointeta.v b/test-suite/failure/fixpointeta.v
new file mode 100644
index 0000000000..9af719322f
--- /dev/null
+++ b/test-suite/failure/fixpointeta.v
@@ -0,0 +1,70 @@
+
+Set Primitive Projections.
+
+Record R := C { p : nat }.
+(* R is defined
+p is defined *)
+
+Unset Primitive Projections.
+Record R' := C' { p' : nat }.
+
+
+
+Fail Definition f := fix f (x : R) : nat := p x.
+(** Not allowed to make fixpoint defs on (non-recursive) records
+ having eta *)
+
+Fail Definition f := fix f (x : R') : nat := p' x.
+(** Even without eta (R' is not primitive here), as long as they're
+ found to be BiFinite (non-recursive), we disallow it *)
+
+(*
+
+(* Subject reduction failure example, if we allowed fixpoints *)
+
+Set Primitive Projections.
+
+Record R := C { p : nat }.
+
+Definition f := fix f (x : R) : nat := p x.
+
+(* eta rule for R *)
+Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x
+ := v.
+
+Definition goal := forall x, f x = p x.
+
+(* when we compute the Rtr away typechecking will fail *)
+Definition thing : goal := fun x =>
+(Rtr (fun x => f x = p x) x (eq_refl _)).
+
+Definition thing' := Eval compute in thing.
+
+Fail Check (thing = thing').
+(*
+The command has indeed failed with message:
+The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
+while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)"
+and "f x = p x").
+*)
+
+Definition thing_refl := eq_refl thing.
+
+Fail Definition thing_refl' := Eval compute in thing_refl.
+(*
+The command has indeed failed with message:
+Illegal application:
+The term "@eq_refl" of type "forall (A : Type) (x : A), x = x"
+cannot be applied to the terms
+ "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop"
+ "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
+The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)"
+which should be coercible to
+ "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)".
+ *)
+
+Definition more_refls : thing_refl = thing_refl.
+Proof.
+ compute. reflexivity.
+Fail Defined. Abort.
+ *)
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index 89556ee75f..dc1397aff2 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -9,6 +9,7 @@
(************************************************************************)
(** Compatibility file for making Coq act similar to Coq v8.7 *)
+Require Export Coq.Compat.Coq88.
(* In 8.7, omega wasn't taking advantage of local abbreviations,
see bug 148 and PR#768. For adjusting this flag, we're forced to
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
new file mode 100644
index 0000000000..4142af05d2
--- /dev/null
+++ b/theories/Compat/Coq88.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.8 *)
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 727fd3ec37..e9f64542c1 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -23,6 +23,7 @@ MLFILES := $(COQMF_MLFILES)
ML4FILES := $(COQMF_ML4FILES)
MLPACKFILES := $(COQMF_MLPACKFILES)
MLLIBFILES := $(COQMF_MLLIBFILES)
+CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES)
INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
OTHERFLAGS := $(COQMF_OTHERFLAGS)
COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS)
@@ -30,6 +31,7 @@ OCAMLLIBS := $(COQMF_OCAMLLIBS)
SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS)
COQLIBS := $(COQMF_COQLIBS)
COQLIBS_NOML := $(COQMF_COQLIBS_NOML)
+CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS)
LOCAL := $(COQMF_LOCAL)
COQLIB := $(COQMF_COQLIB)
DOCDIR := $(COQMF_DOCDIR)
@@ -724,9 +726,14 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+# If this makefile is created using a _CoqProject we have coqdep get
+# options from it. This avoids argument length limits for pathological
+# projects. Note that extra options might be on the command line.
+VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
+
$(VDFILE).d: $(VFILES)
$(SHOW)'COQDEP VFILES'
- $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok)
+ $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
# Misc ########################################################################
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ef4428755a..6cd520d607 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -13,6 +13,8 @@
open CoqProject_file
open Printf
+let (>) f g = fun x -> g (f x)
+
let output_channel = ref stdout
let makefile_name = ref "Makefile"
let make_name = ref ""
@@ -175,21 +177,22 @@ let generate_conf_extra_target oc sps =
in
if sps <> [] then
section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)";
- List.iter pr_path sps
+ List.iter (forget_source > pr_path) sps
let generate_conf_subdirs oc sds =
if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
- List.iter (fprintf oc ".PHONY:%s\n") sds;
- List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
- List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
- List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
- List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
+ let iter f = List.iter (forget_source > f) in
+ iter (fprintf oc ".PHONY:%s\n") sds;
+ iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
+ iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
+ iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
+ iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
section oc "Path directives (-I, -R, -Q).";
let module S = String in
- let open List in
+ let map = map_sourced_list in
let dash1 opt v = sprintf "-%s %s" opt (quote v) in
let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in
fprintf oc "COQMF_OCAMLLIBS = %s\n"
@@ -202,7 +205,11 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
(S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes));
fprintf oc "COQMF_COQLIBS_NOML = %s %s\n"
(S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
- (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
+ (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes));
+ fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n"
+ (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes))
+ (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes))
+ (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes));
;;
let windrive s =
@@ -219,10 +226,10 @@ let generate_conf_coq_config oc args =
;;
let generate_conf_files oc
- { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files }
+ { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; }
=
let module S = String in
- let open List in
+ let map = map_sourced_list in
section oc "Project files.";
fprintf oc "COQMF_VFILES = %s\n" (S.concat " " (map quote v_files));
fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files));
@@ -230,6 +237,8 @@ let generate_conf_files oc
fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files));
fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files));
+ let cmdline_vfiles = filter_cmdline v_files in
+ fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles));
;;
let rec all_start_with prefix = function
@@ -246,12 +255,12 @@ let rec logic_gcd acc = function
else acc
let generate_conf_doc oc { defs; q_includes; r_includes } =
- let includes = List.map snd (q_includes @ r_includes) in
+ let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
let logpaths = List.map (CString.split '.') includes in
let gcd = logic_gcd [] logpaths in
let root =
if gcd = [] then
- if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin
+ if not (List.exists (fun x -> fst x.thing = "INSTALLDEFAULTROOT") defs) then begin
let destination = "orphan_" ^ (String.concat "_" includes) in
eprintf "Warning: no common logical root\n";
eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n";
@@ -264,9 +273,9 @@ let generate_conf_doc oc { defs; q_includes; r_includes } =
let generate_conf_defs oc { defs; extra_args } =
section oc "Extra variables.";
- List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs;
+ List.iter (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs;
Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
- (String.concat " " extra_args)
+ (String.concat " " (List.map forget_source extra_args))
let generate_conf oc project args =
fprintf oc "# This configuration file was generated by running:\n";
@@ -284,10 +293,10 @@ let ensure_root_dir
({ ml_includes; r_includes; q_includes;
v_files; ml_files; mli_files; ml4_files;
mllib_files; mlpack_files } as project)
-=
- let open List in
+ =
+ let exists f = List.exists (forget_source > f) in
let here = Sys.getcwd () in
- let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
+ let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in
if exists (fun { canonical_path = x } -> x = here) ml_includes
|| exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
|| exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
@@ -297,29 +306,27 @@ let ensure_root_dir
then
project
else
+ let source x = {thing=x; source=CmdLine} in
let here_path = { path = "."; canonical_path = here } in
{ project with
- ml_includes = here_path :: ml_includes;
- r_includes = (here_path, "Top") :: r_includes }
+ ml_includes = source here_path :: ml_includes;
+ r_includes = source (here_path, "Top") :: r_includes }
;;
let warn_install_at_root_directory
- { q_includes; r_includes;
- v_files; ml_files; mli_files; ml4_files;
- mllib_files; mlpack_files }
+ ({ q_includes; r_includes; } as project)
=
let open CList in
let inc_top_p =
map_filter
- (fun ({ path } ,ldir) -> if ldir = "" then Some path else None)
+ (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None)
(r_includes @ q_includes) in
- let files =
- v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in
- let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in
+ let files = all_files project in
+ let bad = filter (fun f -> mem (Filename.dirname f.thing) inc_top_p) files in
if bad <> [] then begin
eprintf "Warning: No file should be installed at the root of Coq's library.\n";
eprintf "Warning: No logical path (-R, -Q) applies to these files:\n";
- List.iter (fun x -> eprintf "Warning: %s\n" x) bad;
+ List.iter (fun x -> eprintf "Warning: %s\n" x.thing) bad;
eprintf "\n";
end
;;
@@ -328,10 +335,10 @@ let check_overlapping_include { q_includes; r_includes } =
let pwd = Sys.getcwd () in
let aux = function
| [] -> ()
- | ({ path; canonical_path }, _) :: l ->
+ | {thing = { path; canonical_path }, _} :: l ->
if not (is_prefix pwd canonical_path) then
eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
- List.iter (fun ({ path = p; canonical_path = cp }, _) ->
+ List.iter (fun {thing={ path = p; canonical_path = cp }, _} ->
if is_prefix canonical_path cp || is_prefix cp canonical_path then
eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
path p) l
@@ -354,7 +361,7 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
clean_path (physical_dir_of_logical_dir logic ^ "/" ^
chop_prefix canonical_path file_dir ^ "/") in
let candidates =
- CList.map_filter (fun ({ canonical_path }, logic) ->
+ CList.map_filter (fun {thing={ canonical_path }, logic} ->
if is_prefix canonical_path file_dir then
Some(mk_destination logic canonical_path)
else None) includes
@@ -364,10 +371,10 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
(* BACKWARD COMPATIBILITY: -I into the only logical root *)
begin match
r_includes,
- List.find (fun { canonical_path = p } -> is_prefix p file_dir)
+ List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir)
ml_includes
with
- | [{ canonical_path }, logic], { canonical_path = p } ->
+ | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
let destination =
clean_path (physical_dir_of_logical_dir logic ^ "/" ^
chop_prefix p file_dir ^ "/") in
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f4f143b3b0..12b5cab0ac 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -446,6 +446,7 @@ let usage () =
eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
eprintf " -sort : output the given file name ordered by dependencies\n";
eprintf " -noglob | -no-glob : \n";
+ eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE.";
eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n";
eprintf " -I dir : add (non recursively) dir to ocaml path\n";
eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *)
@@ -462,6 +463,19 @@ let usage () =
let split_period = Str.split (Str.regexp (Str.quote "."))
+let add_q_include path l = add_rec_dir_no_import add_known path (split_period l)
+
+let add_r_include path l = add_rec_dir_import add_known path (split_period l)
+
+let treat_coqproject f =
+ let open CoqProject_file in
+ let iter_sourced f = List.iter (fun {thing} -> f thing) in
+ let project = read_project_file f in
+ iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes;
+ iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes;
+ iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes;
+ iter_sourced (fun f -> treat_file None f) (all_files project)
+
let rec parse = function
| "-c" :: ll -> option_c := true; parse ll
| "-D" :: ll -> option_D := true; parse ll
@@ -469,10 +483,11 @@ 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
+ | "-f" :: f :: ll -> treat_coqproject f; parse ll
| "-I" :: r :: ll -> add_caml_dir r; parse ll
| "-I" :: [] -> usage ()
- | "-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" :: r :: ln :: ll -> add_r_include r ln; parse ll
+ | "-Q" :: r :: ln :: ll -> add_q_include r 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
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c839ed0c70..131b1fab66 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -425,7 +425,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
str "Not enough abstractions in the definition"
| RecursionNotOnInductiveType c ->
str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++
- spc () ++ str "which should be an inductive type"
+ spc () ++ str "which should be a recursive inductive type"
| RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
let arg_env = make_all_name_different arg_env sigma in
let called =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:39:15 +0000