Revision c66987f5f4247e2c68505445eece70390bca5c16 authored by Théo Winterhalter on 27 September 2019, 09:33:02 UTC, committed by GitHub on 27 September 2019, 09:33:02 UTC
Using Prop stuff for eq_universe
| File | Mode | Size |
|---|---|---|
| plugin-demo | ||
| CheckerTest.v | -rw-r--r-- | 333 bytes |
| Makefile | -rw-r--r-- | 257 bytes |
| TypingTests.v | -rw-r--r-- | 4.5 KB |
| _CoqProject | -rw-r--r-- | 594 bytes |
| add_constructor.v | -rw-r--r-- | 3.6 KB |
| bug1.v | -rw-r--r-- | 404 bytes |
| bug2.v | -rw-r--r-- | 175 bytes |
| bug5.v | -rw-r--r-- | 140 bytes |
| bug6.v | -rw-r--r-- | 169 bytes |
| bug7.v | -rw-r--r-- | 200 bytes |
| bug8.v | -rw-r--r-- | 112 bytes |
| bugkncst.v | -rw-r--r-- | 2.7 KB |
| case.v | -rw-r--r-- | 316 bytes |
| castprop.v | -rw-r--r-- | 678 bytes |
| cofix.v | -rw-r--r-- | 144 bytes |
| demo.v | -rw-r--r-- | 11.1 KB |
| erasure_test.v | -rw-r--r-- | 1.4 KB |
| evars.v | -rw-r--r-- | 253 bytes |
| extractable.v | -rw-r--r-- | 2.5 KB |
| hnf_ctor.v | -rw-r--r-- | 159 bytes |
| issue27.v | -rw-r--r-- | 144 bytes |
| issue28.v | -rw-r--r-- | 1.2 KB |
| letin.v | -rw-r--r-- | 286 bytes |
| mutind.v | -rw-r--r-- | 673 bytes |
| opaque.v | -rw-r--r-- | 248 bytes |
| proj.v | -rw-r--r-- | 630 bytes |
| run_in_tactic.v | -rw-r--r-- | 292 bytes |
| safechecker_test.v | -rw-r--r-- | 17.1 KB |
| test_term.v | -rw-r--r-- | 453 bytes |
| tmExistingInstance.v | -rw-r--r-- | 210 bytes |
| tmInferInstance.v | -rw-r--r-- | 255 bytes |
| unfold.v | -rw-r--r-- | 106 bytes |
| univ.v | -rw-r--r-- | 6.5 KB |
| vs.v | -rwxr-xr-x | 74.8 KB |
Computing file changes ...
