]> matita.cs.unibo.it Git - helm.git/commitdiff
Test pretty printg of declarative tactics
authorAndrea Berlingieri <andrea.berlingieri42@gmail.com>
Thu, 26 Sep 2019 20:33:51 +0000 (22:33 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Sep 2019 13:58:08 +0000 (15:58 +0200)
Fix indentation in grafiteAstPp.ml and matitaEnginge.ml with ocp-indent

Add a comment and remove dead code in declarative.ml

Turn off automation weakenings

Generate new .depend files for ng_tactics, syntax_extensions

Add a function that prints a tactic term with the user defined notation
in applyTransformation

Add a function that pretty prints the tactics ASTs to a file while a
script is being parsed and executed


No differences found