diff options
| -rw-r--r-- | interp/implicit_quantifiers.ml | 9 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 24 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 11 |
3 files changed, 31 insertions, 13 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8f42d76c2..c86a2428c 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -31,15 +31,12 @@ let ids_of_list l = let locate_reference qid = match Nametab.extended_locate qid with - | TrueGlobal ref -> ref - | SyntacticDef kn -> - match Syntax_def.search_syntactic_definition dummy_loc kn with - | [],ARef ref -> ref - | _ -> raise Not_found + | TrueGlobal ref -> true + | SyntacticDef kn -> true let is_global id = try - let _ = locate_reference (make_short_qualid id) in true + locate_reference (make_short_qualid id) with Not_found -> false diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 2061d00a5..6a8d0d36d 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -437,6 +437,7 @@ let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") let iff = lazy (gen_constant ["Init"; "Logic"] "iff") +let coq_all = lazy (gen_constant ["Init"; "Logic"] "all") let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") @@ -727,6 +728,14 @@ let unfold_id t = | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_id) *) -> b | _ -> assert false +let unfold_all t = + match kind_of_term t with + | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) -> + (match kind_of_term b with + | Lambda (n, ty, b) -> mkProd (n, ty, b) + | _ -> assert false) + | _ -> assert false + type rewrite_flags = { under_lambdas : bool } let default_flags = { under_lambdas = true } @@ -782,6 +791,21 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars = with Not_found -> None) in res, occ + | Prod (n, ty, b) -> + let lam = mkLambda (n, ty, b) in + let lam', occ = aux env lam occ None in + let res = + match lam' with + | None -> None + | Some (prf, (car, rel, c1, c2)) -> + try + Some (resolve_morphism env sigma t + ~fnewt:unfold_all + (Lazy.force coq_all) [| ty ; lam |] [| None; lam' |] + cstr evars) + with Not_found -> None + in res, occ + | Lambda (n, t, b) when flags.under_lambdas -> let env' = Environ.push_rel (n, None, t) env in refresh_hypinfo env' sigma hypinfo; diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index cb32b846d..0c663b709 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -36,9 +36,7 @@ Definition default_relation [ DefaultRelation A R ] : relation A := R. Notation " x ===def y " := (default_relation x y) (at level 70, no associativity). -Notation "'inverse' R" := (flip (R:relation _) : relation _) (at level 0). - -(* Definition inverse {A} : relation A -> relation A := flip. *) +Notation inverse R := (flip (R:relation _) : relation _). Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. @@ -219,7 +217,7 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid Definition relation_equivalence {A : Type} : relation (relation A) := fun (R R' : relation A) => forall x y, R x y <-> R' x y. -Infix "<R>" := relation_equivalence (at level 70) : relation_scope. +Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. Class subrelation {A:Type} (R R' : relation A) := is_subrelation : forall x y, R x y -> R' x y. @@ -231,12 +229,12 @@ Infix "-R>" := subrelation (at level 70) : relation_scope. Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := fun x y => R x y /\ R' x y. -Infix "/R\" := relation_conjunction (at level 55) : relation_scope. +Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := fun x y => R x y \/ R' x y. -Infix "\R/" := relation_disjunction (at level 55) : relation_scope. +Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. Open Local Scope relation_scope. @@ -288,4 +286,3 @@ Proof. firstorder. Qed. Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). Proof. firstorder. Qed. - |