changes.txt

Changes done by regular expressions:
add @[hott] before definition, lemma, proposition, theorem
shorten definition to def
change `intro x y` to `intros x y`
remove [constructor] [unfold_full] and [unfold *] attributes
change `Type` to `Type _`.
\([^0-9a-z*._₀₁₂₃₄]\)Type\([^0-9a-z*._₀₁₂₃₄]\) -> \1Type _\2, (also avoid `-[`)
Type₀ -> Type
Type₁ -> Type 1
\([^0-9a-z*._₀₁₂₃₄]\)Type.{\([^\}]*\)} -> \1Type \2
protected @[hott] -> @[hott] protected


Manual changes:
put hott_theory at the top of the file
replace !foo by foo _ _ 
replace cases p by induction p
replace x =[p] y with x =[p; P] y, where P is the type family
remove esimp or replace by dsimp
change rewrite with rwr, and remove the syntax which is now unsupported (like +), replace -foo with ←foo
change tac1: tac2 with tac1, all_goals {tac2}
change generalize e, intro x with hgeneralize : e = x
fix all remaining errors. The unification algorithm is less powerful, so sometimes you have to give some more information. Also, coercions aren't inserted very well yet.