diff options
| -rw-r--r-- | backend/RTLgen.v | 4 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 4 | ||||
| -rw-r--r-- | common/AST.v | 6 | ||||
| -rw-r--r-- | common/Errors.v | 2 | ||||
| -rw-r--r-- | cparser/validator/Automaton.v | 6 | ||||
| -rw-r--r-- | cparser/validator/Interpreter.v | 4 | ||||
| -rw-r--r-- | lib/Axioms.v | 6 | ||||
| -rw-r--r-- | lib/Maps.v | 4 |
8 files changed, 17 insertions, 19 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 11da630b..cfbf57d6 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -107,8 +107,8 @@ Inductive res (A: Type) (s: state): Type := | Error: Errors.errmsg -> res A s | OK: A -> forall (s': state), state_incr s s' -> res A s. -Implicit Arguments OK [A s]. -Implicit Arguments Error [A s]. +Arguments OK [A s]. +Arguments Error [A s]. Definition mon (A: Type) : Type := forall (s: state), res A s. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 71b67f67..8725edd1 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -38,8 +38,8 @@ Inductive result (A: Type) (g: generator) : Type := | Err: Errors.errmsg -> result A g | Res: A -> forall (g': generator), Ple (gen_next g) (gen_next g') -> result A g. -Implicit Arguments Err [A g]. -Implicit Arguments Res [A g]. +Arguments Err [A g]. +Arguments Res [A g]. Definition mon (A: Type) := forall (g: generator), result A g. diff --git a/common/AST.v b/common/AST.v index e6fdec3c..34f29bb3 100644 --- a/common/AST.v +++ b/common/AST.v @@ -260,8 +260,8 @@ Inductive globdef (F V: Type) : Type := | Gfun (f: F) | Gvar (v: globvar V). -Implicit Arguments Gfun [F V]. -Implicit Arguments Gvar [F V]. +Arguments Gfun [F V]. +Arguments Gvar [F V]. Record program (F V: Type) : Type := mkprogram { prog_defs: list (ident * globdef F V); @@ -530,7 +530,7 @@ Inductive fundef (F: Type): Type := | Internal: F -> fundef F | External: external_function -> fundef F. -Implicit Arguments External [F]. +Arguments External [F]. Section TRANSF_FUNDEF. diff --git a/common/Errors.v b/common/Errors.v index 293b7993..28933313 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -47,7 +47,7 @@ Inductive res (A: Type) : Type := | OK: A -> res A | Error: errmsg -> res A. -Implicit Arguments Error [A]. +Arguments Error [A]. (** To automate the propagation of errors, we use a monadic style with the following [bind] operation. *) diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v index 98ab1246..fc995298 100644 --- a/cparser/validator/Automaton.v +++ b/cparser/validator/Automaton.v @@ -102,9 +102,9 @@ Module Types(Import Init:AutInit). T term = last_symb_of_non_init_state s -> lookahead_action term | Reduce_act: production -> lookahead_action term | Fail_act: lookahead_action term. - Implicit Arguments Shift_act [term]. - Implicit Arguments Reduce_act [term]. - Implicit Arguments Fail_act [term]. + Arguments Shift_act [term]. + Arguments Reduce_act [term]. + Arguments Fail_act [term]. Inductive action := | Default_reduce_act: production -> action diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v index a24362f8..4ac02693 100644 --- a/cparser/validator/Interpreter.v +++ b/cparser/validator/Interpreter.v @@ -26,8 +26,8 @@ Inductive result (A:Type) := | Err: result A | OK: A -> result A. -Implicit Arguments Err [A]. -Implicit Arguments OK [A]. +Arguments Err [A]. +Arguments OK [A]. Definition bind {A B: Type} (f: result A) (g: A -> result B): result B := match f with diff --git a/lib/Axioms.v b/lib/Axioms.v index 6ae8669a..fdc89920 100644 --- a/lib/Axioms.v +++ b/lib/Axioms.v @@ -39,15 +39,13 @@ Proof @FunctionalExtensionality.functional_extensionality. is an alias for [functional_extensionality]. *) Lemma extensionality: - forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g. + forall {A B: Type} (f g : A -> B), (forall x, f x = g x) -> f = g. Proof @functional_extensionality. -Implicit Arguments extensionality. - (** * Proof irrelevance *) (** We also use proof irrelevance. *) Axiom proof_irr: ClassicalFacts.proof_irrelevance. -Implicit Arguments proof_irr. +Arguments proof_irr [A]. @@ -190,8 +190,8 @@ Module PTree <: TREE. | Leaf : tree A | Node : tree A -> option A -> tree A -> tree A. - Implicit Arguments Leaf [A]. - Implicit Arguments Node [A]. + Arguments Leaf [A]. + Arguments Node [A]. Scheme tree_ind := Induction for tree Sort Prop. Definition t := tree. |