]> matita.cs.unibo.it Git - helm.git/commit
Optional callbacks have been added to tactics that need to introduce
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jan 2003 10:19:55 +0000 (10:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jan 2003 10:19:55 +0000 (10:19 +0000)
commit898a2c9e9c11d5455e9b27069327530db568570d
tree79a0cae46fbc2267fc7fc1acdceda228d0dff0dc
parentabe5665c13b45e51d972c97ad9005ecdc20d206a
Optional callbacks have been added to tactics that need to introduce
new fresh names directly (i.e. without calling other tactics that need
fresh names). The default behaviour is _MUCH_ nicer than the previous
dummy one and is fully functional.

Corollary 1: all the code of tactics.cma is now reentrant.
Corollary 2: the user can be asked the fresh name if it is requested
             by a top-level tactic.
14 files changed:
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/proofEngine.mli
helm/ocaml/tactics/eliminationTactics.ml
helm/ocaml/tactics/eliminationTactics.mli
helm/ocaml/tactics/equalityTactics.ml
helm/ocaml/tactics/fourierR.ml
helm/ocaml/tactics/negationTactics.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/primitiveTactics.mli
helm/ocaml/tactics/proofEngineHelpers.ml
helm/ocaml/tactics/proofEngineHelpers.mli
helm/ocaml/tactics/proofEngineTypes.ml
helm/ocaml/tactics/variousTactics.ml