Skip to content

C
cpdt
Commit b96a9952 authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Fix Extensional type annotations

parent 92fbb06e
Hide whitespace changes
Inline Side-by-side
Showing with 6 additions and 2 deletions
src/Extensional.v
View file @ b96a9952
...@@ -527,7 +527,9 @@ Module PatMatch. ...@@ -527,7 +527,9 @@ Module PatMatch.
: (forall ts, member ts tss -> option (hlist typeDenote ts)) : (forall ts, member ts tss -> option (hlist typeDenote ts))
-> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
-> typeDenote t2 := -> typeDenote t2 :=
match tss with match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
-> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
-> _ with
| nil => fun _ _ => | nil => fun _ _ =>
default default
| ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
...@@ -799,7 +801,9 @@ Module PatMatch. ...@@ -799,7 +801,9 @@ Module PatMatch.
: (forall ts, member ts tss -> pat t1 ts) : (forall ts, member ts tss -> pat t1 ts)
-> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2) -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
-> choice_tree var t1 (option (Elab.exp var t2)) := -> choice_tree var t1 (option (Elab.exp var t2)) :=
match tss with match tss return (forall ts, member ts tss -> pat t1 ts)
-> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
-> _ with
| nil => fun _ _ => | nil => fun _ _ =>
everywhere (fun _ => None) everywhere (fun _ => None)
| ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
......
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