aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES.md5
-rw-r--r--clib/cUnix.ml4
-rw-r--r--clib/cUnix.mli4
-rw-r--r--lib/coqProject_file.ml2
-rw-r--r--plugins/cc/ccalgo.ml3
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/firstorder/g_ground.mlg2
-rw-r--r--plugins/firstorder/rules.ml21
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/funind/indfun_common.ml13
-rw-r--r--plugins/funind/indfun_common.mli3
-rw-r--r--plugins/ltac/tacsubst.ml13
-rw-r--r--plugins/syntax/r_syntax.ml4
-rw-r--r--plugins/syntax/r_syntax.mli9
-rw-r--r--test-suite/bugs/closed/bug_4771.v21
-rw-r--r--test-suite/bugs/closed/bug_8224.v9
-rw-r--r--theories/Compat/Coq88.v3
-rw-r--r--theories/Strings/Ascii.v2
-rw-r--r--theories/Strings/String.v2
-rw-r--r--vernac/comFixpoint.ml15
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comProgramFixpoint.ml17
22 files changed, 72 insertions, 88 deletions
diff --git a/CHANGES.md b/CHANGES.md
index 267a2e2d32..c830bc7a1c 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -175,8 +175,9 @@ Standard Library
- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
and `int31` are no longer available merely by `Require`ing the files
- that define the inductives. You must `Import` `Coq.Strings.String`,
- `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
+ that define the inductives. You must `Import` `Coq.Strings.String.StringSyntax`
+ (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after
+ `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
`Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
`Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
these notations. Note that passing `-compat 8.8` or issuing
diff --git a/clib/cUnix.ml b/clib/cUnix.ml
index 6b42e3041d..eedd878f93 100644
--- a/clib/cUnix.ml
+++ b/clib/cUnix.ml
@@ -74,10 +74,6 @@ let canonical_path_name p =
let make_suffix name suffix =
if Filename.check_suffix name suffix then name else (name ^ suffix)
-let get_extension f =
- let pos = try String.rindex f '.' with Not_found -> String.length f in
- String.sub f pos (String.length f - pos)
-
let correct_path f dir =
if Filename.is_relative f then Filename.concat dir f else f
diff --git a/clib/cUnix.mli b/clib/cUnix.mli
index 1b185345be..896ccd4ea7 100644
--- a/clib/cUnix.mli
+++ b/clib/cUnix.mli
@@ -38,10 +38,6 @@ val path_to_list : string -> string list
[file] does not already end with [suf]. *)
val make_suffix : string -> string -> string
-(** Return the extension of a file, i.e. its smaller suffix starting
- with "." if any, or "" otherwise. *)
-val get_extension : string -> string
-
val file_readable_p : string -> bool
(** {6 Executing commands } *)
diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml
index d0b01453a0..7395654022 100644
--- a/lib/coqProject_file.ml
+++ b/lib/coqProject_file.ml
@@ -220,7 +220,7 @@ let process_cmd_line orig_dir proj args =
let f = CUnix.correct_path f orig_dir in
let proj =
if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
- else match CUnix.get_extension f with
+ else match Filename.extension f with
| ".v" ->
{ proj with v_files = proj.v_files @ [sourced f] }
| ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index f26ec0f401..a6f432b5bd 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -333,9 +333,6 @@ let get_representative uf i=
let get_constructors uf i= uf.map.(i).constructors
-let find_pac uf i pac =
- PacMap.find pac (get_constructors uf i)
-
let rec find_oldest_pac uf i pac=
try PacMap.find pac (get_constructors uf i) with
Not_found ->
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 4ebc6a135a..d52e83dc31 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -145,8 +145,6 @@ val tail_pac : pa_constructor -> pa_constructor
val find : forest -> int -> int
-val find_pac : forest -> int -> pa_constructor -> int
-
val find_oldest_pac : forest -> int -> pa_constructor -> int
val term : forest -> int -> term
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index b9274cf6b8..1128a78093 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -89,8 +89,6 @@ END
{
-let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
-
let gen_ground_tac flag taco ids bases =
let backup= !qflag in
Proofview.tclOR begin
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b0c4785d7a..832a98b7f8 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -21,7 +21,6 @@ open Termops
open Formula
open Sequent
open Globnames
-open Locus
module NamedDecl = Context.Named.Declaration
@@ -56,10 +55,6 @@ let wrap n b continue seq =
continue seq2
end
-let basename_of_global=function
- VarRef id->id
- | _->assert false
-
let clear_global=function
VarRef id-> clear [id]
| _->tclIDTAC
@@ -230,19 +225,3 @@ let ll_forall_tac prod backtrack id continue seq=
backtrack
(* rules for instantiation with unification moved to instances.ml *)
-
-(* special for compatibility with old Intuition *)
-
-let constant str = Coqlib.lib_ref str
-
-let defined_connectives = lazy
- [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type"));
- AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))]
-
-let normalize_evaluables=
- Proofview.Goal.enter begin fun gl ->
- unfold_in_concl (Lazy.force defined_connectives) <*>
- tclMAP
- (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
- (pf_ids_of_hyps gl)
- end
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 924c26790c..97bc992b26 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -22,8 +22,6 @@ type 'a with_backtracking = tactic -> 'a
val wrap : int -> bool -> seqtac
-val basename_of_global: GlobRef.t -> Id.t
-
val clear_global: GlobRef.t -> tactic
val axiom_tac : constr -> Sequent.t -> tactic
@@ -51,5 +49,3 @@ val forall_tac : seqtac with_backtracking
val left_exists_tac : pinductive -> lseqtac with_backtracking
val ll_forall_tac : types -> lseqtac with_backtracking
-
-val normalize_evaluables : tactic
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 28a9542167..cd2ea3ef88 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -27,10 +27,6 @@ let array_get_start a =
(Array.length a - 1)
(fun i -> a.(i))
-let id_of_name = function
- Name id -> id
- | _ -> raise Not_found
-
let locate qid = Nametab.locate qid
let locate_ind ref =
@@ -105,15 +101,6 @@ let const_of_id id =
CErrors.user_err ~hdr:"IndFun.const_of_id"
(str "cannot find " ++ Id.print id)
-let def_of_const t =
- match Constr.kind t with
- Const sp ->
- (try (match Environ.constant_opt_value_in (Global.env()) sp with
- | Some c -> c
- | _ -> assert false)
- with Not_found -> assert false)
- |_ -> assert false
-
[@@@ocaml.warning "-3"]
let coq_constant s =
UnivGen.constr_of_monomorphic_global @@
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1b4c1248a5..0c8f40c5cf 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -18,8 +18,6 @@ val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
val array_get_start : 'a array -> 'a array
-val id_of_name : Name.t -> Id.t
-
val locate_ind : Libnames.qualid -> inductive
val locate_constant : Libnames.qualid -> Constant.t
val locate_with_msg :
@@ -38,7 +36,6 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
val chop_rprod_n : int -> Glob_term.glob_constr ->
(Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
-val def_of_const : Constr.t -> Constr.t
val eq : EConstr.constr Lazy.t
val refl_equal : EConstr.constr Lazy.t
val const_of_id: Id.t -> GlobRef.t(* constantyes *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4626378db6..9173e23b89 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -88,20 +88,9 @@ let subst_reference subst =
(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
to the syntactic non-terminals "global", used in commands such as
Print. It is also used for non-evaluable references. *)
-open Pp
-open Printer
let subst_global_reference subst =
- let subst_global ref =
- let ref',t' = subst_global subst ref in
- if not (is_global ref' t') then
- (let sigma, env = Pfedit.get_current_context () in
- Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
- str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++
- pr_global ref'));
- ref'
- in
- subst_or_var (subst_located subst_global)
+ subst_or_var (subst_located (subst_global_reference subst))
let subst_evaluable subst =
let subst_eval_ref = subst_evaluable_reference subst in
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 776d2a2229..d90b7d754c 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -34,10 +34,8 @@ let is_gr c gr = match DAst.get c with
| _ -> false
let positive_modpath = MPfile (make_dir binnums)
-let positive_path = make_path binnums "positive"
let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
-let glob_positive = IndRef (positive_kn,0)
let path_of_xI = ((positive_kn,0),1)
let path_of_xO = ((positive_kn,0),2)
let path_of_xH = ((positive_kn,0),3)
@@ -71,9 +69,7 @@ let rec bignat_of_pos c = match DAst.get c with
(* Parsing Z via scopes *)
(**********************************************************************)
-let z_path = make_path binnums "Z"
let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
-let glob_z = IndRef (z_kn,0)
let path_of_ZERO = ((z_kn,0),1)
let path_of_POS = ((z_kn,0),2)
let path_of_NEG = ((z_kn,0),3)
diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli
new file mode 100644
index 0000000000..7c3ee60040
--- /dev/null
+++ b/plugins/syntax/r_syntax.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
diff --git a/test-suite/bugs/closed/bug_4771.v b/test-suite/bugs/closed/bug_4771.v
new file mode 100644
index 0000000000..e25e5a1be5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4771.v
@@ -0,0 +1,21 @@
+(* The following code used to trigger an anomaly in functor substitutions *)
+
+Module Type Foo.
+
+Parameter Inline t : nat.
+
+End Foo.
+
+Module F(X : Foo).
+
+Tactic Notation "foo" ref(x) := idtac.
+
+Ltac g := foo X.t.
+
+End F.
+
+Module N.
+Definition t := 0 + 0.
+End N.
+
+Module K := F(N).
diff --git a/test-suite/bugs/closed/bug_8224.v b/test-suite/bugs/closed/bug_8224.v
new file mode 100644
index 0000000000..42dd47d48c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8224.v
@@ -0,0 +1,9 @@
+(* Checking that terms are evar-free before being grounded *)
+
+(* This used to raise an anomaly in 8.9 beta *)
+
+Fail Fixpoint restrict f n :=
+ match n with
+ | O => nil
+ | S n => cons (f n) (restrict f n)
+ end.
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 950cd8242b..0aab64e4c4 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -15,11 +15,10 @@ Require Export Coq.Compat.Coq89.
[Require]. So we make all of the relevant notations accessible in
compatibility mode. *)
Require Coq.Strings.Ascii Coq.Strings.String.
+Export String.StringSyntax Ascii.AsciiSyntax.
Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
Require Coq.Reals.Rdefinitions.
Require Coq.Numbers.Cyclic.Int31.Int31.
-Declare ML Module "string_syntax_plugin".
-Declare ML Module "ascii_syntax_plugin".
Declare ML Module "r_syntax_plugin".
Declare ML Module "int31_syntax_plugin".
Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index d1168694b2..b7c1eaa788 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -23,7 +23,7 @@ Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Register Ascii as plugins.syntax.Ascii.
Declare Scope char_scope.
-Declare ML Module "ascii_syntax_plugin".
+Module Export AsciiSyntax. Declare ML Module "ascii_syntax_plugin". End AsciiSyntax.
Delimit Scope char_scope with char.
Bind Scope char_scope with ascii.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index f6cc8c99ed..a09d518892 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -25,7 +25,7 @@ Inductive string : Set :=
| String : ascii -> string -> string.
Declare Scope string_scope.
-Declare ML Module "string_syntax_plugin".
+Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax.
Delimit Scope string_scope with string.
Bind Scope string_scope with string.
Local Open Scope string_scope.
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 138696e3a7..a9c499b192 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -99,7 +99,7 @@ let check_mutuality env evd isfix fixl =
let names = List.map fst fixl in
let preorder =
List.map (fun (id,def) ->
- (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names))
+ (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names))
fixl in
let po = partial_order Id.equal preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -227,25 +227,28 @@ let interp_recursive ~program_mode ~cofix fixl notations =
(* Instantiate evars and check all are resolved *)
let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
let sigma = Evd.minimize_universes sigma in
- (* XXX: We still have evars here in Program *)
- let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
- let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
(* Build the fix declaration block *)
(env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
- check_evars_are_solved env evd (Evd.from_env env);
if List.for_all Option.has_some fixdefs then begin
let fixdefs = List.map Option.get fixdefs in
check_mutuality env evd isfix (List.combine fixnames fixdefs)
end
+let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
+ check_evars_are_solved env evd (Evd.from_env env);
+ let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
+ let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
+ Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
+
let interp_fixpoint ~cofix l ntns =
let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in
check_recursive true env evd fix;
- (fix,pl,Evd.evar_universe_context evd,info)
+ let uctx,fix = ground_fixpoint env evd fix in
+ (fix,pl,uctx,info)
let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
if List.exists Option.is_empty fixdefs then
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index b1a9c8a5a3..f4569ed3e2 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -51,7 +51,7 @@ val interp_recursive :
(* env / signature / univs / evar_map *)
(Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
(* names / defs / types *)
- (Id.t list * Constr.constr option list * Constr.types list) *
+ (Id.t list * EConstr.constr option list * EConstr.types list) *
(* ctx per mutual def / implicits / struct annotations *)
(EConstr.rel_context * Impargs.manual_explicitation list * int option) list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d533db7ed9..ebedfb1e0d 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
open Pp
open CErrors
open Util
@@ -251,10 +261,10 @@ let do_program_recursive local poly fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
+ EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
and typ =
(* Worrying... *)
- EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
+ EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
@@ -268,6 +278,9 @@ let do_program_recursive local poly fixkind fixl ntns =
let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
let () = if not cofix then begin
let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in
+ (* XXX: are we allowed to have evars here? *)
+ let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in
+ let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in
let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
Array.of_list fixtypes,
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:00:43 +0000