Skip to content

GitLab

Commit 6c233bd4 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

fix for Coq 8.7

parent 6f3b57de
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
theories/base_logic/lib/iprop.v
View file @ 6c233bd4
...@@ -62,8 +62,8 @@ Module gFunctors. ...@@ -62,8 +62,8 @@ Module gFunctors.
Definition app (Σ1 Σ2 : gFunctors) : gFunctors := Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)). existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)).
Global Typeclasses Opaque singleton app.
End gFunctors. End gFunctors.
Typeclasses Opaque gFunctors.singleton gFunctors.app.
Coercion gFunctors.singleton : gFunctor >-> gFunctors. Coercion gFunctors.singleton : gFunctor >-> gFunctors.
Notation "#[ ]" := gFunctors.nil (format "#[ ]"). Notation "#[ ]" := gFunctors.nil (format "#[ ]").
......
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