aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/utile.mli
Commit message (Collapse)AuthorAge
* Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| | | | | | | | | | | | | | | | | | | | | Several cleanups were performed. 1. Removal of dead code lurking around. 2. Removal of global variables used to pass arguments to functions, as well as unnecessary mutable state here and there. We rely on state-passing and encapsulated mutable state. 3. Removal of crazy reference manipulation and its replacement with proper list handling, as well as cleaning up the source and taking advantage of invariants. This should solve algorithmic limitations of the previous code. 4. Opacification of some structures to have a clearer idea of the code requirements. 5. Cleaning of debug printing functions. We thunk the computation of the debugging data, whose computation can be costly for no reason, and we rely on Feedback-based interaction instead of Printf-debugging.
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7
* nsatz ajouteGravatar pottier2010-06-03
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13058 85f007b7-540e-0410-9357-904b9bb8a0f7