Commit 03e6914d authored by POTTIER Francois's avatar POTTIER Francois

The Coq demo does not need MyTactics.

parent 86c981fb
Require Import MyTactics.
Require Import Autosubst.Autosubst.
(* This file is intended as a mini-demonstration of:
......
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