]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years ago- added HBugs support
Stefano Zacchiroli [Thu, 20 Feb 2003 17:27:11 +0000 (17:27 +0000)]
- added HBugs support
- switched to multi threaded implementation
- fixed references from Misc to MQueryMisc module
- moved search pattern apply in ../ocaml/tactics/tacticChaser.ml*

21 years ago- added HBugs notification after tactic application
Stefano Zacchiroli [Thu, 20 Feb 2003 17:24:43 +0000 (17:24 +0000)]
- added HBugs notification after tactic application
- bugfix: removed some useless status save
- defined module type "Tactics", module type returned by Make functor

21 years ago- added dependencies on hbugs-client, threads, helm-mquery_generator
Stefano Zacchiroli [Thu, 20 Feb 2003 17:22:58 +0000 (17:22 +0000)]
- added dependencies on hbugs-client, threads, helm-mquery_generator
- build using -thread switch

21 years agomoved mquery generation in ../ocaml/mquery_generator/
Stefano Zacchiroli [Thu, 20 Feb 2003 17:21:52 +0000 (17:21 +0000)]
moved mquery generation in ../ocaml/mquery_generator/

21 years ago- added and exposed get_current_status_as_xml
Stefano Zacchiroli [Thu, 20 Feb 2003 17:21:05 +0000 (17:21 +0000)]
- added and exposed get_current_status_as_xml
- removed apply_tactic and can_apply_tactic

21 years ago- moved exception IllFormedUri, string_of_cic_textual_parser_uri,
Stefano Zacchiroli [Thu, 20 Feb 2003 17:17:37 +0000 (17:17 +0000)]
- moved exception IllFormedUri, string_of_cic_textual_parser_uri,
  cic_textual_parser_uri_of_string,
  wrong_xpointer_format_from_wrong_xpointer_format' to MQueryMisc
- moved here strip_xml_headings from gTopLevel.ml

21 years agofixed references to functions moved from Misc to MQueryMisc
Stefano Zacchiroli [Thu, 20 Feb 2003 17:16:13 +0000 (17:16 +0000)]
fixed references to functions moved from Misc to MQueryMisc

21 years agoadded HBugs interface module for gTopLevel
Stefano Zacchiroli [Thu, 20 Feb 2003 17:15:24 +0000 (17:15 +0000)]
added HBugs interface module for gTopLevel

21 years agorebuilt
Stefano Zacchiroli [Thu, 20 Feb 2003 17:14:58 +0000 (17:14 +0000)]
rebuilt

21 years agoremoved tmp_dir no longer needed (it was used only by ClientHTTP module)
Stefano Zacchiroli [Wed, 19 Feb 2003 14:29:18 +0000 (14:29 +0000)]
removed tmp_dir no longer needed (it was used only by ClientHTTP module)

21 years agobugfix: use temporary file name to avoid file access clashes when the
Stefano Zacchiroli [Wed, 19 Feb 2003 14:28:56 +0000 (14:28 +0000)]
bugfix: use temporary file name to avoid file access clashes when the
same teporary dir is used by many processes

21 years ago- added pp_to_outchan and pp_to_string for other medium pretty printing
Stefano Zacchiroli [Wed, 19 Feb 2003 14:27:34 +0000 (14:27 +0000)]
- added pp_to_outchan and pp_to_string for other medium pretty printing
- factorized implementation of pretty printers so that it's used by all
  pretty printing functions

21 years agoMakefile patched
Ferruccio Guidi [Wed, 5 Feb 2003 14:04:06 +0000 (14:04 +0000)]
Makefile patched

21 years agoMakefile.common.in and .depend backtracked to my last commit (before the
Claudio Sacerdoti Coen [Wed, 5 Feb 2003 12:46:20 +0000 (12:46 +0000)]
Makefile.common.in and .depend backtracked to my last commit (before the
ones of Ferruccio) and then modified. Dependencies between a file and a
library are now handled correctly.

21 years agopackege dependences calculation patched
Ferruccio Guidi [Wed, 5 Feb 2003 11:42:52 +0000 (11:42 +0000)]
packege dependences calculation patched

21 years agopackage dependences calulation fixed
Ferruccio Guidi [Wed, 5 Feb 2003 11:09:48 +0000 (11:09 +0000)]
package dependences calulation fixed

21 years agoSQL quoting fixed in relation.ml
Ferruccio Guidi [Tue, 4 Feb 2003 19:08:28 +0000 (19:08 +0000)]
SQL quoting fixed in relation.ml

21 years agoAdded new module DiscriminationTactics
Michele Galatà [Tue, 4 Feb 2003 17:59:06 +0000 (17:59 +0000)]
Added new module DiscriminationTactics

21 years agoAdded buttons for new tactics Injection and Discriminate
Michele Galatà [Tue, 4 Feb 2003 17:51:55 +0000 (17:51 +0000)]
Added buttons for new tactics Injection and Discriminate

21 years agoAdded module DiscriminationTactics with brand new tactics Injection and
Michele Galatà [Tue, 4 Feb 2003 17:50:34 +0000 (17:50 +0000)]
Added module DiscriminationTactics with brand new tactics Injection and
Discriminate, both working only in simple situation

21 years agopatches for the new interface of text_of_query/text_of result
Ferruccio Guidi [Mon, 3 Feb 2003 17:32:56 +0000 (17:32 +0000)]
patches for the new interface of text_of_query/text_of result

21 years agonew interface for text_of_query/text_of_result + bug fixes
Ferruccio Guidi [Mon, 3 Feb 2003 17:27:45 +0000 (17:27 +0000)]
new interface for text_of_query/text_of_result + bug fixes

21 years agoDependency simplification.
Claudio Sacerdoti Coen [Mon, 3 Feb 2003 10:50:45 +0000 (10:50 +0000)]
Dependency simplification.

21 years agoMinor module re-organization:
Claudio Sacerdoti Coen [Mon, 3 Feb 2003 10:50:12 +0000 (10:50 +0000)]
Minor module re-organization:
1. SequentPp is now no more dependent from proofEngine
2. the functions to apply stylesheets from DOM documents to DOM documents
   are not any longer exported by ApplyStylesheets

21 years ago...
Claudio Sacerdoti Coen [Fri, 31 Jan 2003 18:45:15 +0000 (18:45 +0000)]
...

21 years agoThe scratch window is now based on the sequent_viewer widget.
Claudio Sacerdoti Coen [Fri, 31 Jan 2003 18:44:20 +0000 (18:44 +0000)]
The scratch window is now based on the sequent_viewer widget.

21 years agoMajor module reorganization:
Claudio Sacerdoti Coen [Fri, 31 Jan 2003 10:10:21 +0000 (10:10 +0000)]
Major module reorganization:
- new module TermViewer: holds widgets to render and interact with sequents
  and proofs at the CIC level
- new module ApplyStylesheets: functions to apply stylesheets and map
  terms and sequents to MathML Presentation
- new module InvokeTactics: it is a functor that gives back a module that
  defines one callback function for every tactic

21 years ago1. helmns and domImpl moved to the misc module ;-(
Claudio Sacerdoti Coen [Thu, 30 Jan 2003 10:36:05 +0000 (10:36 +0000)]
1. helmns and domImpl moved to the misc module ;-(
2. all the constants and functions relative to stylesheet applications have
   been moved to the new module ApplyStylesheets, whose interface is really
   minimal.

21 years agoMinor code reorganization:
Claudio Sacerdoti Coen [Thu, 30 Jan 2003 09:43:03 +0000 (09:43 +0000)]
Minor code reorganization:
 1. several functions unrelated do disambiguation moved from Disambiguate
    do Misc.
 2. TermEditor module added. It implements a widget for entering terms.
    The widget is also responsible for the disambiguation.
 3. TermEditor is now the only widget that uses the Disambiguate module.

21 years agoTactics button rearranged.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 18:22:16 +0000 (18:22 +0000)]
Tactics button rearranged.

21 years agoClear and ClearBody moved to the pop-up menu.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 18:07:05 +0000 (18:07 +0000)]
Clear and ClearBody moved to the pop-up menu.
No check is done so far to avoid activating them when the selected "term"
is not an hypothesis.

21 years agoreplace_lifting generalized to the simultaneous replacement of n terms.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 18:02:57 +0000 (18:02 +0000)]
replace_lifting generalized to the simultaneous replacement of n terms.

21 years agoProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite".
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 17:09:47 +0000 (17:09 +0000)]
ProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite".

21 years ago1. Added a callback to the generalize tactic to generate a fresh name.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 17:03:27 +0000 (17:03 +0000)]
1. Added a callback to the generalize tactic to generate a fresh name.
2. Dead code removal in various files.

21 years agoAdded a callback to the generalize tactic to generate a fresh name.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 17:02:40 +0000 (17:02 +0000)]
Added a callback to the generalize tactic to generate a fresh name.

21 years agoGeneralize now works on a list of convertible terms, generalizing all of
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 16:54:44 +0000 (16:54 +0000)]
Generalize now works on a list of convertible terms, generalizing all of
them at once.

21 years agoGeneralize tactic moved to the contextual menu.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 16:18:25 +0000 (16:18 +0000)]
Generalize tactic moved to the contextual menu.

21 years agoNew: we now have a new pop-up menu for the reduction tactics.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 16:07:28 +0000 (16:07 +0000)]
New: we now have a new pop-up menu for the reduction tactics.

21 years ago1. All the reduction tactics have been modified to reduce several (sub)terms
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 13:20:55 +0000 (13:20 +0000)]
1.  All the reduction tactics have been modified to reduce several (sub)terms
    at once.
2.  To reduce several (sub)terms at once you can use the new multiple
    selection feature.

21 years agoAll the reduction tactics have been modified to reduce several (sub)terms
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 13:20:00 +0000 (13:20 +0000)]
All the reduction tactics have been modified to reduce several (sub)terms
at once.

21 years agoMultiple selection is now enabled in the goal and check windows.
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 12:02:37 +0000 (12:02 +0000)]
Multiple selection is now enabled in the goal and check windows.
All the tactics still behave as before.

21 years agomaction toggle restored
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 11:13:00 +0000 (11:13 +0000)]
maction toggle restored

21 years agoOptional callbacks have been added to tactics that need to introduce
Claudio Sacerdoti Coen [Wed, 29 Jan 2003 10:19:55 +0000 (10:19 +0000)]
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.

21 years agoDead code removed.
Claudio Sacerdoti Coen [Tue, 28 Jan 2003 18:40:46 +0000 (18:40 +0000)]
Dead code removed.

21 years agoDecompose now has a new parameter which is the callback to call to select the
Claudio Sacerdoti Coen [Tue, 28 Jan 2003 18:38:45 +0000 (18:38 +0000)]
Decompose now has a new parameter which is the callback to call to select the
uris that must be used for the decomposition.

21 years agoDecompose now has a new parameter that is the callback function to call
Claudio Sacerdoti Coen [Tue, 28 Jan 2003 18:37:54 +0000 (18:37 +0000)]
Decompose now has a new parameter that is the callback function to call
to select the uris that must be decomposed.

21 years agoFixed. It was no more working since the move of the tactics under the ocaml
Claudio Sacerdoti Coen [Tue, 28 Jan 2003 17:30:33 +0000 (17:30 +0000)]
Fixed. It was no more working since the move of the tactics under the ocaml
repository.

21 years agoadded META for module helm-tactics
Stefano Zacchiroli [Tue, 28 Jan 2003 10:23:59 +0000 (10:23 +0000)]
added META for module helm-tactics

21 years agomoved tactics from gTopLevel to the new module ocaml/tactics
Stefano Zacchiroli [Tue, 28 Jan 2003 10:23:03 +0000 (10:23 +0000)]
moved tactics from gTopLevel to the new module ocaml/tactics

21 years agomoved tactics in ocaml/tactics
Stefano Zacchiroli [Tue, 28 Jan 2003 10:22:00 +0000 (10:22 +0000)]
moved tactics in ocaml/tactics

21 years ago* very small fixes here and there
Luca Padovani [Mon, 27 Jan 2003 14:32:07 +0000 (14:32 +0000)]
* very small fixes here and there

21 years agoAdded Decompose tactic
Michele Galatà [Fri, 24 Jan 2003 11:15:57 +0000 (11:15 +0000)]
Added Decompose tactic

21 years agobugfix while printing MutInd and MutConstruct unresolved uris
Stefano Zacchiroli [Tue, 21 Jan 2003 16:37:09 +0000 (16:37 +0000)]
bugfix while printing MutInd and MutConstruct unresolved uris

21 years agoadded html templates and pages
Stefano Zacchiroli [Tue, 21 Jan 2003 11:38:40 +0000 (11:38 +0000)]
added html templates and pages

21 years ago- disambiguation implemented!
Stefano Zacchiroli [Tue, 21 Jan 2003 11:37:12 +0000 (11:37 +0000)]
- disambiguation implemented!

21 years ago- added references to gTopLevel needed modules
Stefano Zacchiroli [Tue, 21 Jan 2003 11:36:07 +0000 (11:36 +0000)]
- added references to gTopLevel needed modules

21 years agoNew module Disambiguate to hold:
Claudio Sacerdoti Coen [Tue, 21 Jan 2003 11:24:52 +0000 (11:24 +0000)]
New module Disambiguate to hold:
 - a functor to disambiguate terms. The input module holds all the
   callbacks to the user (that will be implemented differently in Gtk
   and as Web forms).
 - some utility functions working on CicTextualParser0.uri which should
   be moved somewhere else.

21 years agotypo: ')' mismatch
Stefano Zacchiroli [Sun, 5 Jan 2003 13:59:16 +0000 (13:59 +0000)]
typo: ')' mismatch

21 years agoAmbiguous parsing improved: refining is now used to prune-out not-well-typed
Claudio Sacerdoti Coen [Mon, 23 Dec 2002 21:36:52 +0000 (21:36 +0000)]
Ambiguous parsing improved: refining is now used to prune-out not-well-typed
choices as soon as the term can not be refined. Unfortunately the whole
disambiguation is parsing-bound and not type-checking/refining bound.

21 years agoRefine can now also raise Uncertain. The exception is raised every
Claudio Sacerdoti Coen [Mon, 23 Dec 2002 21:07:55 +0000 (21:07 +0000)]
Refine can now also raise Uncertain. The exception is raised every
time a metavariab le could be instantiated in such a way that the
term could become well-typed. Useful for ambiguous parsing.

21 years agoThe interpretation function can now return also "Implicit".
Claudio Sacerdoti Coen [Mon, 23 Dec 2002 21:06:04 +0000 (21:06 +0000)]
The interpretation function can now return also "Implicit".
Useful for incremental ambiguous parsing.

21 years agoNew: refinement is now used to disambiguate parsing.
Claudio Sacerdoti Coen [Sun, 22 Dec 2002 19:06:27 +0000 (19:06 +0000)]
New: refinement is now used to disambiguate parsing.

21 years agoNew constructs \x.T and !x.T introduced. They require refinement.
Claudio Sacerdoti Coen [Sun, 22 Dec 2002 19:05:38 +0000 (19:05 +0000)]
New constructs \x.T and !x.T introduced. They require refinement.

21 years ago* First implementation of CicRefine
Claudio Sacerdoti Coen [Sun, 22 Dec 2002 19:04:49 +0000 (19:04 +0000)]
* First implementation of CicRefine
* unwind_subst is now exported in the interface

21 years ago* if no configuration file is found, issue a warning but doesn't crash
Luca Padovani [Fri, 20 Dec 2002 15:10:20 +0000 (15:10 +0000)]
* if no configuration file is found, issue a warning but doesn't crash

21 years ago"Insert Query (Experts only)" menu item added.
Claudio Sacerdoti Coen [Wed, 18 Dec 2002 17:33:10 +0000 (17:33 +0000)]
"Insert Query (Experts only)" menu item added.

21 years agoAdded a special charcount threatment to the 'append' csymbol (whose length
Claudio Sacerdoti Coen [Fri, 13 Dec 2002 15:05:25 +0000 (15:05 +0000)]
Added a special charcount threatment to the 'append' csymbol (whose length
was estimated being 6 instead of 3). We should do the same for every csymbol
we provide special notation to.

21 years agoMathQL textual lexer patched
Ferruccio Guidi [Fri, 13 Dec 2002 12:39:01 +0000 (12:39 +0000)]
MathQL textual lexer patched
topLevel patched for compilation: -B and -MB don't work

21 years agoWrong commit undone.
Claudio Sacerdoti Coen [Fri, 13 Dec 2002 10:02:28 +0000 (10:02 +0000)]
Wrong commit undone.

21 years agoLast commit before major modifications to do.
Andrea Asperti [Fri, 13 Dec 2002 09:58:48 +0000 (09:58 +0000)]
Last commit before major modifications to do.

21 years agoRearranged tactics in VariousTactics into new modules EliminationTactics,
Michele Galatà [Fri, 13 Dec 2002 09:27:05 +0000 (09:27 +0000)]
Rearranged tactics in VariousTactics into new modules EliminationTactics,
EqualityTactics, IntroductionTactics and NegationTactics.

21 years agoMinor widget rearrangement.
Claudio Sacerdoti Coen [Thu, 12 Dec 2002 18:53:12 +0000 (18:53 +0000)]
Minor widget rearrangement.

21 years agonotation "@" for append added
Claudio Sacerdoti Coen [Thu, 12 Dec 2002 18:43:45 +0000 (18:43 +0000)]
notation "@" for append added

21 years agoAdded an almost working version of Generalize tactic.
Michele Galatà [Thu, 12 Dec 2002 15:36:00 +0000 (15:36 +0000)]
Added an almost working version of Generalize tactic.

21 years agoAdded an almost working version of Generalize tactic.
Michele Galatà [Thu, 12 Dec 2002 15:22:09 +0000 (15:22 +0000)]
Added an almost working version of Generalize tactic.
Added yet another version of replace, useful in Generalize.

21 years agoRearranged tactics in VariousTactics into new modules EqualityTactics, EliminationTac...
Michele Galatà [Thu, 12 Dec 2002 09:08:38 +0000 (09:08 +0000)]
Rearranged tactics in VariousTactics into new modules EqualityTactics, EliminationTactics,
IntroductionTactics and NegationTactics.
Added new tactics: Rewrite <-, Replace.

21 years agoSevere bug fixed: the test failed in the case of (Rplus (...) R1).
Claudio Sacerdoti Coen [Wed, 11 Dec 2002 11:43:18 +0000 (11:43 +0000)]
Severe bug fixed: the test failed in the case of (Rplus (...) R1).
As a consequence (Rplus (Rplus R1 R1) R1) was rendered as 2.

21 years ago* Partial checking of mutual inductive definitions allowed.
Claudio Sacerdoti Coen [Wed, 11 Dec 2002 10:48:13 +0000 (10:48 +0000)]
* Partial checking of mutual inductive definitions allowed.
* New environment variables requested:
   GTOPLEVEL_PROOFFILE
   GTOPLEVEL_PROOFFILETYPE
   GTOPLEVEL_PROOFFILE
   GTOPLEVEL_PROOFFILETYPE
   POSTGRESQL_CONNECTION_STRING

21 years agoUnary minus now rendered without parentheses.
Claudio Sacerdoti Coen [Wed, 11 Dec 2002 10:37:39 +0000 (10:37 +0000)]
Unary minus now rendered without parentheses.

21 years ago"Rewrite ... with ... by ..." line-breaking handled.
Claudio Sacerdoti Coen [Tue, 10 Dec 2002 18:49:15 +0000 (18:49 +0000)]
"Rewrite ... with ... by ..." line-breaking handled.

21 years agoFirst experimental commit of the notation (partial!) for real numbers.
Claudio Sacerdoti Coen [Tue, 10 Dec 2002 17:50:45 +0000 (17:50 +0000)]
First experimental commit of the notation (partial!) for real numbers.

21 years agoRing partially ported to the new library. But I am completely sure that
Claudio Sacerdoti Coen [Tue, 10 Dec 2002 17:04:13 +0000 (17:04 +0000)]
Ring partially ported to the new library. But I am completely sure that
this is not the notation we need for ring. To be changed...

21 years agoBug fixed: beta-redex transformations to LetIn were bugged when the lambda
Claudio Sacerdoti Coen [Tue, 10 Dec 2002 17:03:12 +0000 (17:03 +0000)]
Bug fixed: beta-redex transformations to LetIn were bugged when the lambda
had two or more decls.

21 years agocut & paste typo fixed
Claudio Sacerdoti Coen [Tue, 10 Dec 2002 17:02:12 +0000 (17:02 +0000)]
cut & paste typo fixed

21 years agopositive.xsl is now included in headercontent.xsl and no more required in
Claudio Sacerdoti Coen [Tue, 10 Dec 2002 16:58:44 +0000 (16:58 +0000)]
positive.xsl is now included in headercontent.xsl and no more required in
arith.xml and list.xml. This is necessary to overload the standard rendering
of some operators (e.g. notation for real numbers).

21 years agoNow "only" constraint are more restrictive.
natile [Mon, 9 Dec 2002 12:08:46 +0000 (12:08 +0000)]
Now "only" constraint are more restrictive.

21 years ago* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed
Claudio Sacerdoti Coen [Mon, 9 Dec 2002 10:53:29 +0000 (10:53 +0000)]
* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed
  only in the conclusion and not (yet) on the hypothesis.

21 years ago* New button "Select only constants" to choose the URIs to try during the
Claudio Sacerdoti Coen [Mon, 9 Dec 2002 10:52:34 +0000 (10:52 +0000)]
* New button "Select only constants" to choose the URIs to try during the
  disambiguation phase. Usually the number of constants is small and among
  them there is the right URI.
* New ElimIntrosSimpl replaces the old ElimSimplIntros.

21 years agoSimpl now handles let-in reductions as delta-reductions. Cool.
Claudio Sacerdoti Coen [Mon, 9 Dec 2002 10:50:18 +0000 (10:50 +0000)]
Simpl now handles let-in reductions as delta-reductions. Cool.

21 years ago* mQueryLevel2.get_constraints now gives back only the "must" constraints.
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 18:43:09 +0000 (18:43 +0000)]
* mQueryLevel2.get_constraints now gives back only the "must" constraints.
* the "refine constraints" interface has been improved. It can now handle
  also constraints on Sorts and constants.

21 years agoNew notation for ListSet. It often raises ambiguity problems in theorems
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 17:57:34 +0000 (17:57 +0000)]
New notation for ListSet. It often raises ambiguity problems in theorems
that also use the same notation for PolyLists.

21 years agoinstantiate for inductive principles covered
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 16:05:48 +0000 (16:05 +0000)]
instantiate for inductive principles covered

21 years agoinstantiate for induction principles covered.
Andrea Asperti [Fri, 6 Dec 2002 16:04:07 +0000 (16:04 +0000)]
instantiate for induction principles covered.

21 years agoBug fixed in binary standard MathML Content operators: the href/xref
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 15:00:53 +0000 (15:00 +0000)]
Bug fixed in binary standard MathML Content operators: the href/xref
attributes were not generated.

21 years ago...
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 14:57:28 +0000 (14:57 +0000)]
...

21 years agoThe fresh_name generator has been moved to ProofEngineHelpers.
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 13:36:07 +0000 (13:36 +0000)]
The fresh_name generator has been moved to ProofEngineHelpers.
intros_tac now directly uses it ==> no more ~mkname arguments.
The generator has been "improved" so that it does not generate any
more two equal names. The drawback is that every identifier is
augmented with a nonce.

21 years agoComments removed.
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 13:33:46 +0000 (13:33 +0000)]
Comments removed.

21 years agoBug fixed: when iota-expanding fixpoints the context was sometimes augmented
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 13:31:28 +0000 (13:31 +0000)]
Bug fixed: when iota-expanding fixpoints the context was sometimes augmented
with the new types, even if the expansion already de-lifted the function body.

21 years agomQueryLevels2.mli added in Makefile.
natile [Fri, 6 Dec 2002 13:31:17 +0000 (13:31 +0000)]
mQueryLevels2.mli added in Makefile.

21 years agoThe user interface for the completeSearchPattern query has been improved.
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 13:18:47 +0000 (13:18 +0000)]
The user interface for the completeSearchPattern query has been improved.
It is now "easy" to query for induction principles, for example.
Much work still to do.