aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/implicit_quantifiers.ml19
-rw-r--r--interp/implicit_quantifiers.mli6
-rw-r--r--theories/Classes/Morphisms_Relations.v2
-rw-r--r--theories/Classes/RelationClasses.v2
-rw-r--r--theories/MSets/MSetAVL.v4
-rw-r--r--theories/MSets/MSetInterface.v2
-rw-r--r--theories/MSets/MSetList.v4
-rw-r--r--theories/MSets/MSetWeakList.v4
9 files changed, 28 insertions, 19 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0f593e67c3..0057edad6d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -842,7 +842,7 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
Implicit_quantifiers.combine_params_freevar ty
in
let ty' = intern_type (ids,true,tmpsc,sc) ty in
- let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty' in
+ let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
let na = match na with
@@ -879,7 +879,7 @@ let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((id
let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
let c = intern (ids,true,tmp_scope,scopes) c in
- let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
+ let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in
let env', c' =
let abs =
let pi =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index dc2f8ad0aa..f9ac88e6bc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -95,13 +95,17 @@ let is_freevar ids env x =
(* Auxilliary functions for the inference of implicitly quantified variables. *)
+let ungeneralizable loc id =
+ user_err_loc (loc, "Generalization",
+ str "Unbound and ungeneralizable variable " ++ pr_id id)
+
let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
let found loc id bdvars l =
if List.mem id l then 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 ungeneralizable loc id
else l
in
let rec aux bdvars l c = match c with
@@ -134,7 +138,7 @@ let add_name_to_ids set na =
| Anonymous -> set
| Name id -> Idset.add id set
-let free_vars_of_rawconstr ?(bound=Idset.empty) =
+let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) =
let rec vars bound vs = function
| RVar (loc,id) ->
if is_freevar bound (Global.env ()) id then
@@ -191,15 +195,16 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) =
and vars_return_type bound vs (na,tyopt) =
let bound' = add_name_to_ids bound na in
vars_option bound' vs tyopt
- in
- fun rt -> List.rev (vars bound [] rt)
+ in fun rt ->
+ let vars = List.rev (vars bound [] rt) in
+ List.iter (fun (id, loc) ->
+ if not (Idset.mem id allowed || find_generalizable_ident id) then
+ ungeneralizable loc id) vars;
+ vars
let rec make_fresh ids env x =
if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
-let fre_ids env ids =
- List.filter (is_freevar env (Global.env())) ids
-
let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
let next_name_away_from na avoid =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 8f02eb7658..1feae81f56 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,9 +38,11 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
val free_vars_of_binders :
?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
-(* Returns the free ids in left-to-right order with the location of their first occurence *)
+(* Returns the generalizable free ids in left-to-right
+ order with the location of their first occurence *)
-val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
+ rawconstr -> (Names.identifier * loc) list
val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 9c42ff155c..d8365abc79 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -16,6 +16,8 @@ Require Import Relation_Definitions.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.Program.
+Generalizable Variables A l.
+
(** Morphisms for relations *)
Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 06da511292..2caaa063a5 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -74,7 +74,7 @@ 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.
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
Proof. tauto. Qed.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 477c431c42..8f825c5841 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -538,7 +538,7 @@ Definition IsOk := bst.
Class Ok (s:t) : Prop := { ok : bst s }.
-Instance bst_Ok `(Hs : bst s) : Ok s := Hs.
+Instance bst_Ok s (Hs : bst s) : Ok s := Hs.
Fixpoint ltb_tree x s :=
match s with
@@ -657,7 +657,7 @@ Proof.
intuition_in.
Qed.
-Instance isok_Ok `(isok s = true) : Ok s | 10.
+Instance isok_Ok s : isok s = true -> Ok s | 10.
Proof. intros; apply <- isok_iff; auto. Qed.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index ef32c114b2..a2a686d94d 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -342,7 +342,7 @@ Module Type WRawSets (E : DecidableType).
predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
always-false function. *)
Parameter isok : t -> bool.
- Instance isok_Ok `(isok s = true) : Ok s | 10.
+ Instance isok_Ok s `(isok s = true) : Ok s | 10.
(** Logical predicates *)
Parameter In : elt -> t -> Prop.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 8b0a16c112..b7b9a024a9 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -225,7 +225,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Hint Resolve @ok.
Hint Constructors Ok.
- Instance Sort_Ok `(Hs : Sort s) : Ok s := Hs.
+ Instance Sort_Ok s `(Hs : Sort s) : Ok s := Hs.
Ltac inv_ok := match goal with
| H:Ok (_ :: _) |- _ => apply @ok in H; inversion_clear H; inv_ok
@@ -276,7 +276,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
constructor; intuition.
Qed.
- Global Instance isok_Ok `(isok s = true) : Ok s | 10.
+ Global Instance isok_Ok s `(isok s = true) : Ok s | 10.
Proof.
intros. apply <- isok_iff. auto.
Qed.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index d5a85e6c2a..0af8a24aa4 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -126,7 +126,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
Hint Constructors Ok.
Hint Resolve @ok.
- Instance NoDup_Ok `(nd : NoDup s) : Ok s := nd.
+ Instance NoDup_Ok s (nd : NoDup s) : Ok s := nd.
Ltac inv_ok := match goal with
| H:Ok (_ :: _) |- _ => apply @ok in H; inversion_clear H; inv_ok
@@ -179,7 +179,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
rewrite <- mem_spec; auto; congruence.
Qed.
- Global Instance isok_Ok `(isok l = true) : Ok l | 10.
+ Global Instance isok_Ok l : isok l = true -> Ok l | 10.
Proof.
intros. apply <- isok_iff; auto.
Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:08:37 +0000