diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Utils.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index c4a20506c7..149901c7bb 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -42,8 +42,8 @@ Notation dec := sumbool_of_bool. (** Hide proofs and generates obligations when put in a term. *) -Notation "'in_left'" := (@left _ _ _) : program_scope. -Notation "'in_right'" := (@right _ _ _) : program_scope. +Notation in_left := (@left _ _ _). +Notation in_right := (@right _ _ _). (** Extraction directives *) (* @@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) (* Extract Inductive sigT => "prod" [ "" ]. *) -*)
\ No newline at end of file +*) |