aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml1
-rw-r--r--interp/implicit_quantifiers.ml56
-rw-r--r--interp/implicit_quantifiers.mli2
-rw-r--r--parsing/g_vernac.ml49
-rw-r--r--parsing/ppvernac.ml11
-rw-r--r--plugins/interface/xlate.ml1
-rw-r--r--theories/Classes/EquivDec.v2
-rw-r--r--theories/Classes/Equivalence.v2
-rw-r--r--theories/Classes/Functions.v2
-rw-r--r--theories/Classes/Morphisms.v2
-rw-r--r--theories/Classes/RelationClasses.v2
-rw-r--r--theories/Classes/SetoidAxioms.v2
-rw-r--r--theories/Classes/SetoidClass.v2
-rw-r--r--theories/Classes/SetoidDec.v2
-rw-r--r--theories/Classes/SetoidTactics.v4
-rw-r--r--theories/Logic/Diaconescu.v2
-rw-r--r--theories/MSets/MSetFacts.v2
-rw-r--r--theories/Structures/OrderedType2.v2
-rw-r--r--tools/coq_makefile.ml44
-rw-r--r--toplevel/vernacentries.ml3
-rw-r--r--toplevel/vernacexpr.ml1
21 files changed, 102 insertions, 12 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index eb410b1e3..11d8a3061 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -274,6 +274,7 @@ let rec attribute_of_vernac_command = function
| VernacSyntacticDefinition _ -> []
| VernacDeclareImplicits _ -> []
| VernacReserve _ -> []
+ | VernacGeneralizable _ -> []
| VernacSetOpacity _ -> []
| VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
| VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a55daff36..93f4eedff 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -24,8 +24,49 @@ open Libnames
open Typeclasses
open Typeclasses_errors
open Pp
+open Libobject
+open Nameops
(*i*)
+let generalizable_table = ref Idpred.empty
+
+let _ =
+ Summary.declare_summary "generalizable-ident"
+ { Summary.freeze_function = (fun () -> !generalizable_table);
+ Summary.unfreeze_function = (fun r -> generalizable_table := r);
+ Summary.init_function = (fun () -> generalizable_table := Idpred.empty) }
+
+let declare_generalizable_ident table (loc,id) =
+ if id <> root_of_id id then
+ user_err_loc(loc,"declare_generalizable_ident",
+ (pr_id id ++ str
+ " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
+ if Idpred.mem id table then
+ user_err_loc(loc,"declare_generalizable_ident",
+ (pr_id id++str" is already declared as a generalizable identifier"))
+ else Idpred.add id table
+
+let add_generalizable gen table =
+ match gen with
+ | None -> Idpred.empty
+ | Some [] -> Idpred.full
+ | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid)
+ table l
+
+let cache_generalizable_type (_,(local,cmd)) =
+ generalizable_table := add_generalizable cmd !generalizable_table
+
+let (in_generalizable, _) =
+ declare_object {(default_object "GENERALIZED-IDENT") with
+ cache_function = cache_generalizable_type;
+ classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
+ }
+
+let declare_generalizable local gen =
+ Lib.add_anonymous_leaf (in_generalizable (local, gen))
+
+let find_generalizable_ident id = Idpred.mem (root_of_id id) !generalizable_table
+
let ids_of_list l =
List.fold_right Idset.add l Idset.empty
@@ -51,13 +92,16 @@ let is_freevar ids env x =
(* Auxilliary functions for the inference of implicitly quantified variables. *)
let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
- let found id bdvars l =
+ let found loc id bdvars l =
if List.mem id l then l
- else if not (is_freevar bdvars (Global.env ()) id)
- then l else id :: l
+ else if is_freevar bdvars (Global.env ()) id
+ then
+ if find_generalizable_ident id then id :: l
+ else user_err_loc (loc, "Generalization", str "Unbound and ungeneralizable variable " ++ pr_id id)
+ else l
in
let rec aux bdvars l c = match c with
- | CRef (Ident (_,id)) -> found id bdvars l
+ | CRef (Ident (loc,id)) -> found loc id bdvars l
| CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
| c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
@@ -204,14 +248,14 @@ let combine_params_freevar =
let destClassApp cl =
match cl with
- | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
+ | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l
| CAppExpl (loc, (None, ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
let destClassAppExpl cl =
match cl with
- | CApp (loc, (None,CRef ref), l) -> loc, ref, l
+ | CApp (loc, (None, CRef ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 0d28eccad..8f02eb765 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -24,6 +24,8 @@ open Libnames
open Typeclasses
(*i*)
+val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
+
val ids_of_list : identifier list -> Idset.t
val destClassApp : constr_expr -> loc * reference * constr_expr list
val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e1a71ff23..52cb3d898 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -518,7 +518,7 @@ GEXTEND Gram
pri = OPT [ "|"; i = natural -> i ] ;
props = [ ":="; "{"; r = record_declaration; "}" -> r |
":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
- VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
+ VernacInstance (not (use_section_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
| IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
@@ -545,7 +545,12 @@ GEXTEND Gram
VernacDeclareImplicits (use_section_locality (),qid,pos)
| IDENT "Implicit"; ["Type" | IDENT "Types"];
- idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
+ idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c)
+
+ | IDENT "Generalizable"; ["Variable" | IDENT "Variables"];
+ gen = [ IDENT "none" -> None | IDENT "all" -> Some [] |
+ idl = LIST1 identref -> Some idl ] ->
+ VernacGeneralizable (use_section_locality (), gen) ] ]
;
implicit_name:
[ [ "!"; id = ident -> (id, false, true)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 76098e4fb..8a8248bf4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -831,7 +831,8 @@ let rec pr_vernac = function
(pr_locality local ++ str "Ltac " ++
prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
| VernacCreateHintDb (local,dbname,b) ->
- hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
+ hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++
+ str dbname ++ (if b then str" discriminated" else mt ()))
| VernacHints (local,dbnames,h) ->
pr_hints local dbnames h pr_constr pr_constr_pattern_expr
| VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
@@ -851,6 +852,14 @@ let rec pr_vernac = function
str (if List.length idl > 1 then "s " else " ") ++
prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++
pr_lconstr c)
+ | VernacGeneralizable (local, g) ->
+ hov 1 (pr_locality local ++ str"Generalizable Variable" ++
+ match g with
+ | None -> str "s none"
+ | Some [] -> str "s all"
+ | Some idl ->
+ str (if List.length idl > 1 then "s " else " ") ++
+ prlist_with_sep spc pr_lident idl)
| VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
hov 1 (str"Transparent" ++ pr_non_locality b ++
spc() ++ prlist_with_sep sep pr_smart_global l)
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index b4e0e69bb..627cd517c 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -2183,6 +2183,7 @@ let rec xlate_vernac =
List.map (fun (_,x) -> xlate_ident x) l),
xlate_formula f)
| VernacReserve([], _) -> assert false
+ | VernacGeneralizable (_, _) -> xlate_error "TODO: Generalizable"
| VernacLocate(LocateTerm id) -> CT_locate(loc_smart_global_to_ct_ID id)
| VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
| VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module"
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index e87482d84..bafbac3f1 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -26,6 +26,8 @@ Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Program.Program.
+Generalizable Variables A B R.
+
Open Scope equiv_scope.
Class DecidableEquivalence `(equiv : Equivalence A) :=
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 78e66d374..cc8d79c03 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -25,6 +25,8 @@ Require Import Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
+Generalizable Variables A R eqA B S eqB.
+
Open Local Scope signature_scope.
Definition equiv `{Equivalence A R} : relation A := R.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 8c6161036..5efa4fa8f 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -17,6 +17,8 @@
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
+Generalizable Variables A B eqA eqB RA RB f.
+
Set Implicit Arguments.
Unset Strict Implicit.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 76da120e0..ac455415e 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -20,6 +20,8 @@ Require Import Coq.Program.Tactics.
Require Import Coq.Relations.Relation_Definitions.
Require Export Coq.Classes.RelationClasses.
+Generalizable Variables all.
+
(** * Morphisms.
We now turn to the definition of [Proper] and declare standard instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0d6130263..cc3cae4da 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -74,6 +74,8 @@ Hint Extern 4 => solve_relation : relations.
(** We can already dualize all these properties. *)
+Generalizable Variables A B C D R S T U eqA eqB eqC eqD.
+
Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
Proof. tauto. Qed.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index ef115b2ed..3789bb66f 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -19,6 +19,8 @@ Require Import Coq.Program.Program.
Set Implicit Arguments.
Unset Strict Implicit.
+Generalizable Variables a.
+
Require Export Coq.Classes.SetoidClass.
(** Application of the extensionality axiom to turn a goal on
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 33d98548d..995b37185 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -17,6 +17,8 @@
Set Implicit Arguments.
Unset Strict Implicit.
+Generalizable Variables A.
+
Require Import Coq.Program.Program.
Require Import Relation_Definitions.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 32e75adae..33b4350f8 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -18,6 +18,8 @@
Set Implicit Arguments.
Unset Strict Implicit.
+Generalizable Variables A B .
+
(** Export notations. *)
Require Export Coq.Classes.SetoidClass.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index c40e37e24..669be8b0f 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -18,6 +18,8 @@ Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
Require Import Coq.Classes.Equivalence Coq.Program.Basics.
+Generalizable Variables A R.
+
Export ProperNotations.
Set Implicit Arguments.
@@ -177,3 +179,5 @@ Ltac default_add_morphism_tactic :=
Ltac add_morphism_tactic := default_add_morphism_tactic.
Obligation Tactic := program_simpl.
+
+(* Notation "'Morphism' s t " := (@Proper _ (s%signature) t) (at level 10, s at next level, t at next level). *)
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 22c838c26..18f3181b6 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -39,7 +39,7 @@
[Bell93] John L. Bell, Hilbert's epsilon operator and classical
logic, Journal of Philosophical Logic, 22: 1-18, 1993
- [Carlström04] Jesper Carlström, [EM + Ext_ + AC_int <-> AC_ext],
+ [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
*)
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index 2ba969217..bd99198f4 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -489,6 +489,8 @@ Qed.
(* [fold], [filter], [for_all], [exists_] and [partition] requires
some knowledge on [f] in order to be known as morphisms. *)
+Generalizable Variables f.
+
Instance filter_equal `(Proper _ (E.eq==>Logic.eq) f) :
Proper (Equal==>Equal) (filter f).
Proof.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index fdb1ccc24..c72d3a79d 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -270,6 +270,8 @@ Definition FstRel {A B}(R:relation A) : relation (A*B) :=
Definition SndRel {A B}(R:relation B) : relation (A*B) :=
fun p p' => R (snd p) (snd p').
+Generalizable Variables A B RA RB Ri Ro.
+
Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) :
Equivalence (ProdRel RA RB).
Proof. firstorder. Qed.
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 486c8804f..31af75fee 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -402,10 +402,10 @@ let main_targets vfiles mlfiles other_targets inc =
print "spec: $(VIFILES)\n\n";
print "gallina: $(GFILES)\n\n";
print "html: $(GLOBFILES) $(VFILES)\n";
- print "\t- mkdir html\n";
+ print "\t- mkdir -p html\n";
print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
- print "\t- mkdir html\n";
+ print "\t- mkdir -p html\n";
print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "all.ps: $(VFILES)\n";
print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 754f58a9c..70feb6ceb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -771,6 +771,8 @@ let vernac_reserve idl c =
let t = Detyping.detype false [] [] t in
List.iter (fun id -> Reserve.declare_reserved_type id t) idl
+let vernac_generalizable = Implicit_quantifiers.declare_generalizable
+
let make_silent_if_not_pcoq b =
if !pcoq <> None then
error "Turning on/off silent flag is not supported in Pcoq mode."
@@ -1375,6 +1377,7 @@ let interp c = match c with
| VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
| VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
| VernacReserve (idl,c) -> vernac_reserve idl c
+ | VernacGeneralizable (local,gen) -> vernac_generalizable local gen
| VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
| VernacSetOption (locality,key,v) -> vernac_set_option locality key v
| VernacUnsetOption (locality,key) -> vernac_unset_option locality key
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 25642bdc7..2e73767c5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -301,6 +301,7 @@ type vernac_expr =
| VernacDeclareImplicits of locality_flag * reference or_by_notation *
(explicitation * bool * bool) list option
| VernacReserve of lident list * constr_expr
+ | VernacGeneralizable of locality_flag * (lident list) option
| VernacSetOpacity of
locality_flag * (Conv_oracle.level * reference or_by_notation list) list
| VernacUnsetOption of full_locality_flag * Goptions.option_name
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 16:37:35 +0000