Skip to content

GitLab

S
stdpp
Commit 8497827e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Get rid of `Automatic Coercions Import`, it is deprecated.

parent 0e409c0d
Pipeline #4503 passed with stages
      in 3 minutes and 57 seconds
      Show whitespace changes
      Inline Side-by-side
      Showing with 0 additions and 1 deletion
      theories/base.v
      View file @ 8497827e
      ...@@ -5,7 +5,6 @@ that are used throughout the whole development. Most importantly it contains ...@@ -5,7 +5,6 @@ that are used throughout the whole development. Most importantly it contains
      abstract interfaces for ordered structures, collections, and various other data abstract interfaces for ordered structures, collections, and various other data
      structures. *) structures. *)
      Global Generalizable All Variables. Global Generalizable All Variables.
      Global Set Automatic Coercions Import.
      Global Set Asymmetric Patterns. Global Set Asymmetric Patterns.
      Global Unset Transparent Obligations. Global Unset Transparent Obligations.
      From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
      ......
      Markdown is supported
      0% or .
      You are about to add 0 people to the discussion. Proceed with caution.
      Finish editing this message first!
      Please register or to comment