aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common3
-rw-r--r--contrib/subtac/subtac.ml4
-rw-r--r--contrib/subtac/subtac_classes.ml3
-rw-r--r--contrib/subtac/subtac_classes.mli2
-rw-r--r--tactics/class_tactics.ml436
-rw-r--r--theories/Classes/Functions.v43
-rw-r--r--theories/Classes/Init.v3
-rw-r--r--theories/Classes/Morphisms.v16
-rw-r--r--theories/Classes/Relations.v27
-rw-r--r--theories/Classes/SetoidClass.v1
-rw-r--r--theories/Classes/SetoidTactics.v11
-rw-r--r--theories/Init/Wf.v2
-rw-r--r--theories/Program/Basics.v13
-rw-r--r--theories/Program/Wf.v8
-rw-r--r--toplevel/classes.ml9
-rw-r--r--toplevel/classes.mli2
-rw-r--r--toplevel/command.ml29
-rw-r--r--toplevel/command.mli4
-rw-r--r--toplevel/vernacentries.ml2
19 files changed, 169 insertions, 49 deletions
diff --git a/Makefile.common b/Makefile.common
index 1b7a2fef53..73c76e5a43 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -748,7 +748,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor
UNICODEVO:= theories/Unicode/Utf8.vo
CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \
- theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
+ theories/Classes/Functions.vo theories/Classes/Equivalence.vo \
+ theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
THEORIESVO:=\
$(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index f3696f6ec9..e9c2ed4e52 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -100,7 +100,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
- List.iter (Command.declare_one_assumption is_coe k c nl) idl
+ List.iter (Command.declare_one_assumption is_coe k c imps nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
@@ -149,7 +149,7 @@ let subtac (loc, command) =
vernac_assumption env isevars stre l nl
| VernacInstance (sup, is, props) ->
- Subtac_classes.new_instance sup is props
+ ignore(Subtac_classes.new_instance sup is props)
| VernacCoFixpoint (l, b) ->
let _ = trace (str "Building cofixpoint") in
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index fb15e41b6a..e439021635 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -221,4 +221,5 @@ let new_instance ctx (instid, bk, cl) props =
in
let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
- ignore (Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls)
+ ignore(Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls);
+ id
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index f9b36b0c06..12a6e29549 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -36,4 +36,4 @@ val new_instance :
Topconstr.local_binder list ->
typeclass_constraint ->
binder_def_list ->
- unit
+ identifier
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a34853b025..86a1081ec3 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -276,16 +276,21 @@ let valid evm p res_sigma l =
else (gls, sigma))
!res_sigma (l, Evd.create_evar_defs !res_sigma)
in raise (Found (snd evd'))
+
+let refresh_evi evi =
+ { evi with
+(* evar_hyps = Environ.map_named_val Termops.refresh_universes evi.evar_hyps ; *)
+ evar_concl = Termops.refresh_universes evi.evar_concl }
let resolve_all_evars_once debug (mode, depth) env p evd =
let evm = Evd.evars_of evd in
- let goals =
+ let goals, evm =
Evd.fold
- (fun ev evi gls ->
- if evi.evar_body = Evar_empty && p ev evi then
- (evi :: gls)
- else gls)
- evm []
+ (fun ev evi (gls, evm) ->
+ let evi = refresh_evi evi in
+ (if evi.evar_body = Evar_empty && p ev evi then evi :: gls else gls),
+ Evd.add evm ev evi)
+ evm ([], Evd.empty)
in
let gls = { it = List.rev goals; sigma = evm } in
let res_sigma = ref evm in
@@ -691,3 +696,22 @@ END
let _ =
Classes.refine_ref := Refine.refine
+
+open Pretype_errors
+
+let typeclass_error e =
+ match e with
+ | UnsolvableImplicit (evi, (InternalHole | ImplicitArg _)) ->
+ (match class_of_constr evi.evar_concl with
+ Some c -> true
+ | None -> false)
+ | _ -> false
+
+let class_apply c =
+ try Tactics.apply_with_ebindings c
+ with PretypeError (env, e) when typeclass_error e ->
+ tclFAIL 1 (str"typeclass resolution failed")
+
+TACTIC EXTEND class_apply
+| [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ]
+END
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
new file mode 100644
index 0000000000..7942d36427
--- /dev/null
+++ b/theories/Classes/Functions.v
@@ -0,0 +1,43 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Functional morphisms.
+
+ Author: Matthieu Sozeau
+ Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ 91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective :=
+ injective : forall x y : A, RB (f x) (f y) -> RA x y.
+
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective :=
+ surjective : forall y, exists x : A, RB y (f x).
+
+Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+ Injective m /\ Surjective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+ monic :> Injective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+ epic :> Surjective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+ monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
+
+Class [ m : Morphism (A -> A) (eqA ++> eqA), ? IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index beeb745899..cb27fbc380 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -16,3 +16,6 @@
(* $Id: Init.v 616 2007-08-08 12:28:10Z msozeau $ *)
(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
+
+Tactic Notation "clapply" ident(c) :=
+ eapply @c ; eauto with typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3ba6c1824b..18dc3190f2 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -133,6 +133,13 @@ Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl.
+Lemma reflexive_impl_iff [ Symmetric A R, ? Morphism (R ++> impl) m ] : Morphism (R ==> iff) m.
+Proof.
+ intros.
+ constructor ; simpl_relation.
+ split ; clapply respect ; [ idtac | sym ] ; auto.
+Qed.
+
(** The complement of a relation conserves its morphisms. *)
Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
@@ -158,6 +165,15 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
apply respect ; auto.
Qed.
+Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C) ] =>
+ flip_morphism : ? Morphism (RB ++> RA ++> RC) (flip f).
+
+ Next Obligation.
+ Proof.
+ unfold flip.
+ apply respect ; auto.
+ Qed.
+
(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
(* fun x y => R x y -> R' (f x) (f y). *)
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index c05a4b1e12..0d21985dcf 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -17,7 +17,7 @@
(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
Require Import Coq.Program.Program.
-Require Import Coq.Classes.Init.
+Require Export Coq.Classes.Init.
Set Implicit Arguments.
Unset Strict Implicit.
@@ -71,15 +71,15 @@ Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R
Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R).
- Solve Obligations using unfold flip ; program_simpl ; apply symmetric ; eauto.
+ Solve Obligations using unfold flip ; program_simpl ; clapply symmetric.
Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R).
- Solve Obligations using program_simpl ; unfold flip in * ; intros ; eapply asymmetric ; eauto.
+ Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric.
Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R).
- Solve Obligations using unfold flip ; program_simpl ; eapply transitive ; eauto.
+ Solve Obligations using unfold flip ; program_simpl ; clapply transitive.
(** Have to do it again for Prop. *)
@@ -91,15 +91,15 @@ Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irr
Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R).
- Solve Obligations using unfold inverse, flip ; program_simpl ; eapply symmetric ; eauto.
+ Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric.
Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R).
- Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; eapply asymmetric ; eauto.
+ Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric.
Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R).
- Solve Obligations using unfold inverse, flip ; program_simpl ; eapply transitive ; eauto.
+ Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive.
Program Instance [ Reflexive A (R : relation A) ] =>
reflexive_complement_irreflexive : Irreflexive A (complement R).
@@ -190,6 +190,12 @@ Ltac relation_refl :=
| [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?X ] => apply (reflexive (R:=R A B C D E F) X)
| [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F) H)
+
+ | [ |- ?R ?A ?B ?C ?D ?E ?F ?G ?X ?X ] => apply (reflexive (R:=R A B C D E F G) X)
+ | [ H : ?R ?A ?B ?C ?D ?E ?F ?G ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F G) H)
+
+ | [ |- ?R ?A ?B ?C ?D ?E ?F ?G ?H ?X ?X ] => apply (reflexive (R:=R A B C D E F G H) X)
+ | [ H : ?R ?A ?B ?C ?D ?E ?F ?G ?H ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F G H) H)
end.
Ltac refl := relation_refl.
@@ -284,6 +290,12 @@ Ltac trans Y := relation_transitive Y.
Ltac relation_tac := relation_refl || relation_sym || relation_trans.
+(** Various combinations of reflexivity, symmetry and transitivity. *)
+
+Class PreOrder A (R : relation A) :=
+ preorder_refl :> Reflexive R ;
+ preorder_trans :> Transitive R.
+
(** The [PER] typeclass. *)
Class PER (carrier : Type) (pequiv : relation carrier) :=
@@ -340,3 +352,4 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
Equivalence (a -> b)
(fun f g => forall (x y : a), R x y -> R' (f x) (g y)).
*)
+
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index cd7737d06d..9ec955bcfe 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -24,6 +24,7 @@ Unset Strict Implicit.
Require Export Coq.Classes.Relations.
Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.Functions.
(** A setoid wraps an equivalence. *)
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index fb7f8827bf..953296c28c 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -25,17 +25,12 @@ Require Export Coq.Classes.SetoidClass.
(* Application of the extensionality axiom to turn a goal on leibinz equality to
a setoid equivalence. *)
-Lemma setoideq_eq [ sa : Setoid a ] : forall x y : a, x == y -> x = y.
-Proof.
- admit.
-Qed.
-
-Implicit Arguments setoideq_eq [[a] [sa]].
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
(** Application of the extensionality principle for setoids. *)
-Ltac setoideq_ext :=
+Ltac setoid_extensionality :=
match goal with
- [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
+ [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
end.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 6e07ea43a9..87cd9becc0 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -157,7 +157,7 @@ Section Well_founded_2.
P x x' :=
F
(fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
- Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+ Acc_iter_2 (x:=y) (x':=y') (Acc_inv a h)).
End Acc_iter_2.
Hypothesis Rwf : well_founded R.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 3040dd04ba..8a3e5dccd9 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -18,7 +19,7 @@ Unset Strict Implicit.
Require Export Coq.Program.FunctionalExtensionality.
-Notation "'λ' x : T , y" := (fun x:T => y) (at level 1, x,T,y at level 10) : program_scope.
+Notation " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
Open Scope program_scope.
@@ -45,7 +46,7 @@ Proof.
Qed.
Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D),
- h ∘ (g ∘ f) = h ∘ g ∘ f.
+ h ∘ g ∘ f = h ∘ (g ∘ f).
Proof.
intros.
reflexivity.
@@ -117,7 +118,7 @@ Qed.
(** Useful implicits and notations for lists. *)
-Require Export Coq.Lists.List.
+Require Import Coq.Lists.List.
Implicit Arguments nil [[A]].
Implicit Arguments cons [[A]].
@@ -141,3 +142,9 @@ Tactic Notation "exist" constr(x) := exists x.
Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+
+(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
+(* (at level 200, x ident, y ident, right associativity) : program_scope. *)
+
+(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
+(* (at level 200, x ident, right associativity) : program_scope. *) \ No newline at end of file
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 70b1b1b5a2..98b18f9030 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -17,7 +17,7 @@ Section Well_founded.
Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y)
- (Acc_inv r (proj1_sig y) (proj2_sig y))).
+ (Acc_inv r (proj2_sig y))).
Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
End Acc.
@@ -38,7 +38,7 @@ Section Well_founded.
Lemma Fix_F_eq :
forall (x:A) (r:Acc R x),
- F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+ F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
Proof.
destruct r using Acc_inv_dep; auto.
Qed.
@@ -89,7 +89,7 @@ Section Well_founded_measure.
Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y)
- (Acc_inv r (m (proj1_sig y)) (proj2_sig y))).
+ (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))).
Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
@@ -111,7 +111,7 @@ Section Well_founded_measure.
Lemma Fix_measure_F_eq :
forall (x:A) (r:Acc lt (m x)),
- F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r.
+ F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
Proof.
intros x.
set (y := m x).
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ec2c950486..627633ad54 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -493,13 +493,15 @@ let new_instance ctx (instid, bk, cl) props =
in
let kn = Declare.declare_constant id cdecl in
Flags.if_verbose Command.definition_message id;
- hook kn
+ hook kn;
+ Some id
else
let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
(!refine_ref (evm, term));
- Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ()
+ Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
+ None
@@ -529,7 +531,8 @@ let context l =
let sigma = Evd.evars_of !isevars in
let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
List.iter (function (id,_,t) ->
- Command.declare_one_assumption false (Local (* global *), Definitional) t false (* inline *) (dummy_loc, id))
+ Command.declare_one_assumption false (Local (* global *), Definitional) t
+ [] false (* inline *) (dummy_loc, id))
(List.rev fullctx)
open Libobject
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index f305fc805e..809888f0d7 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -43,7 +43,7 @@ val new_instance :
local_binder list ->
typeclass_constraint ->
binder_def_list ->
- unit
+ identifier option
val context : typeclass_context -> unit
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ccdb906cec..ffe4c26d54 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -177,7 +177,7 @@ let syntax_definition ident c local onlyparse =
let assumption_message id =
if_verbose message ((string_of_id id) ^ " is assumed")
-let declare_one_assumption is_coe (local,kind) c nl (_,ident) =
+let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) =
let r = match local with
| Local when Lib.sections_are_opened () ->
let _ =
@@ -191,11 +191,14 @@ let declare_one_assumption is_coe (local,kind) c nl (_,ident) =
| (Global|Local) ->
let kn =
declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
+ let gr = ConstRef kn in
+ if Impargs.is_implicit_args () || imps <> [] then
+ declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
assumption_message ident;
if local=Local & Flags.is_verbose () then
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
str" because it is at a global level");
- ConstRef kn in
+ gr in
if is_coe then Class.try_add_new_coercion r local
let declare_assumption_hook = ref ignore
@@ -204,9 +207,12 @@ let set_declare_assumption_hook = (:=) declare_assumption_hook
let declare_assumption idl is_coe k bl c nl=
if not (Pfedit.refining ()) then
let c = generalize_constr_expr c bl in
- let c = interp_type Evd.empty (Global.env()) c in
- !declare_assumption_hook c;
- List.iter (declare_one_assumption is_coe k c nl) idl
+ let sigma = Evd.empty and env = Global.env () in
+ let ic = intern_type sigma env c in
+ let imps = Implicit_quantifiers.implicits_of_rawterm ic in
+ let j = Default.understand_judgment sigma env ic in
+ !declare_assumption_hook j.uj_val;
+ List.iter (declare_one_assumption is_coe k j.uj_val imps nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
@@ -1026,9 +1032,16 @@ let start_proof_com sopt kind (bl,t) hook =
(Pfedit.get_all_proof_names ())
in
let env = Global.env () in
- let c = interp_type Evd.empty env (generalize_constr_expr t bl) in
- let _ = Typeops.infer_type env c in
- start_proof id kind c hook
+ let sigma = Evd.empty in
+ let b = generalize_constr_expr t bl in
+ let ib = intern_type sigma env b in
+ let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+ let j = Default.understand_judgment sigma env ib in
+ start_proof id kind j.uj_val
+ (fun str cst ->
+ if Impargs.is_implicit_args () || imps <> [] then
+ declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
+ hook str cst)
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2dbc295387..d67daa83a6 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -40,8 +40,8 @@ val declare_definition : identifier -> definition_kind ->
val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
-val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool
- -> Names.variable located -> unit
+val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
+ Impargs.manual_explicitation list -> bool -> Names.variable located -> unit
val set_declare_assumption_hook : (types -> unit) -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 13b2bab5cb..770cc5ccf4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -534,7 +534,7 @@ let vernac_class id par ar sup props =
Classes.new_class id par ar sup props
let vernac_instance sup inst props =
- Classes.new_instance sup inst props
+ ignore(Classes.new_instance sup inst props)
let vernac_context l =
Classes.context l
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:42:48 +0000