Commit 37855c7e authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Got rid of some dumb warnings.

parent aec2b9e5
......@@ -228,7 +228,6 @@ Module FunLMap (L : Locations) <: (LocationMap L).
cbn in *.
destruct (inb l ls2) eqn:eq.
rewrite IHls1'; intros l' i; apply sub; right; auto.
Check inb_spec.
pose proof (proj2 (inb_spec l ls2) (sub l ltac:(left; reflexivity))).
transitivity (inb l ls2); auto.
Qed.
......
......@@ -247,7 +247,7 @@ Module LambdaCalc <: Expression.
| appArgStep : forall e1 e2 e2' : Expr,
LCStep e2 e2'
-> LCStep (app e1 e2) (app e1 e2').
Hint Constructors LCStep : LC.
Global Hint Constructors LCStep : LC.
Definition ExprStep := LCStep.
Theorem ExprClosedBelowSubst : forall (e : Expr) (σ : nat -> Expr) (n : nat),
......
......@@ -40,7 +40,7 @@ Module STLC <: (TypedExpression LambdaCalc).
end) e e ::: τ2
-> Γ e (abs τ1 e) ::: (ArrowT τ1 τ2)
where "Γ ⊢e e ::: τ" := (LCTyping Γ e τ).
Hint Constructors LCTyping : LC.
Global Hint Constructors LCTyping : LC.
Definition ExprTyping := LCTyping.
Definition ExprVarTyping := varTyping.
......
Supports Markdown
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