]> matita.cs.unibo.it Git - helm.git/log
helm.git
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.

21 years ago1. depth constraints for Rels and Sorts are now optional
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 13:17:13 +0000 (13:17 +0000)]
1. depth constraints for Rels and Sorts are now optional
2. "can" constraints renamed to "only" constraints
3. several bug fixes:
    * the order of arguments for Sub in the second phase of the query was wrong
    * some identifiers in the generated query were unbound

21 years ago1. The depth constraint on Rels and Sorts is now optional.
Claudio Sacerdoti Coen [Fri, 6 Dec 2002 13:15:28 +0000 (13:15 +0000)]
1. The depth constraint on Rels and Sorts is now optional.
2. "only" (ex "can") constraints are copies of the "must" constraints

21 years agoA simplification bug was introduced during the clean-up before the last
Claudio Sacerdoti Coen [Thu, 5 Dec 2002 14:57:45 +0000 (14:57 +0000)]
A simplification bug was introduced during the clean-up before the last
commit. Fixed.

21 years agoNotation for if then else.
Andrea Asperti [Thu, 5 Dec 2002 14:43:30 +0000 (14:43 +0000)]
Notation for if then else.
Other bug fixes.

21 years agoBug fixed: the lhs part of an explicit name substitution was not generated
Claudio Sacerdoti Coen [Thu, 5 Dec 2002 14:21:10 +0000 (14:21 +0000)]
Bug fixed: the lhs part of an explicit name substitution was not generated
as an m:ci, but as simple text ===> no m:mi and no hyperlink were generated.

21 years agoMinor bug fixes in the 'instantiate' element handling.
Claudio Sacerdoti Coen [Thu, 5 Dec 2002 13:35:19 +0000 (13:35 +0000)]
Minor bug fixes in the 'instantiate' element handling.

21 years agoShowing a query result which was an inductive type or constructor was bugged.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 18:42:31 +0000 (18:42 +0000)]
Showing a query result which was an inductive type or constructor was bugged.

21 years agoInterface improvement: a window is opened to show objects returned by the
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 18:15:46 +0000 (18:15 +0000)]
Interface improvement: a window is opened to show objects returned by the
completeSearchPattern query.

21 years ago...
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 17:37:47 +0000 (17:37 +0000)]
...

21 years ago*** empty log message ***
natile [Wed, 4 Dec 2002 17:34:58 +0000 (17:34 +0000)]
*** empty log message ***

21 years agoNew feature: the user can now enter the list of "must" constraints he wants.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 16:02:52 +0000 (16:02 +0000)]
New feature: the user can now enter the list of "must" constraints he wants.

21 years ago* mQueryLevels interface clean-up
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 15:38:47 +0000 (15:38 +0000)]
* mQueryLevels interface clean-up
* gui improvement: the precision level of the SearchPattern query is now
  chosen by the user. Previously it was guessed.

21 years agoSimplification euristic improved.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 14:29:52 +0000 (14:29 +0000)]
Simplification euristic improved.
It is now able to simplify a Fix which expands to an expressions which
simplifiable Fixes therein.

21 years agoCompletely broken parsing of Fix and CoFix fixed.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 14:27:22 +0000 (14:27 +0000)]
Completely broken parsing of Fix and CoFix fixed.

21 years agoSeveral bug-fixes to the abstparam hell.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 12:39:45 +0000 (12:39 +0000)]
Several bug-fixes to the abstparam hell.

21 years ago- reverted to only one quotation level for xmluri, libxml2 is now fixed
Stefano Zacchiroli [Wed, 4 Dec 2002 12:39:14 +0000 (12:39 +0000)]
- reverted to only one quotation level for xmluri, libxml2 is now fixed

21 years agoVariable redefined twice fixed.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 11:05:42 +0000 (11:05 +0000)]
Variable redefined twice fixed.

21 years agoVariable redefined twice fixed.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 11:02:46 +0000 (11:02 +0000)]
Variable redefined twice fixed.

21 years agoNew tactic fold_simpl.
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 10:57:07 +0000 (10:57 +0000)]
New tactic fold_simpl.

21 years ago* fold_tac has now a new parameter, which is the reduction to ``undo''
Claudio Sacerdoti Coen [Wed, 4 Dec 2002 10:20:32 +0000 (10:20 +0000)]
* fold_tac has now a new parameter, which is the reduction to ``undo''
* The Fold button is replaced with Fold_whd and Fold_reduce
* Minor interfaces modifications

21 years agoTyping of intros_tac improved. It now has a parameter that is a fresh-names
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 17:47:30 +0000 (17:47 +0000)]
Typing of intros_tac improved. It now has a parameter that is a fresh-names
generator.

21 years agoQuick implementation of the "inst" csymbol. It can surely be improved.
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 17:15:21 +0000 (17:15 +0000)]
Quick implementation of the "inst" csymbol. It can surely be improved.

21 years agoFirst working version of the possibility to introduce new inductive type
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 16:05:50 +0000 (16:05 +0000)]
First working version of the possibility to introduce new inductive type
definitions. Many checks have not been implemented yet and the interface
allows you to progress to further stages even if the input is incorrect.
Nevertheless, if the input is correct it will be accepted by the kernel,
saved to disk and notified to the getter.

This is the dawn of a new set implementation era.

21 years agoput_inductive_definition implemented and exposed.
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 14:50:31 +0000 (14:50 +0000)]
put_inductive_definition implemented and exposed.
It is a very UNSAFE solution to the problem of computing inner-types of
non-debrujined mutual inductive types (whose constructors referes to
the not-yet-defined inductive type block): you can use this function to
add the block to the environment; then you compute the inner-types; and
finally you save the object and register it to the getter.

21 years agotypecheck_mutual_inductive_defs exposed.
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 14:34:05 +0000 (14:34 +0000)]
typecheck_mutual_inductive_defs exposed.
It is used to type-check and inductive definition which has no URI associated
to it (i.e. it is not managed by the getter; e.g. when it is not saved yet
since we do not know if it is well-typed).

21 years agoAn exception was raised when a MutInd or MutConstruct had an uri to a
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 14:30:58 +0000 (14:30 +0000)]
An exception was raised when a MutInd or MutConstruct had an uri to a
non-existing object. The whole URI + XPointer is now printed.

21 years agoAdded new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)
Michele Galatà [Tue, 3 Dec 2002 11:02:33 +0000 (11:02 +0000)]
Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)
Moved ElimType from ring.ml to variousTactics.ml
Moved Contradiction from fourierR.ml to variousTactics.ml

21 years agom:exist ==> m:exists
Claudio Sacerdoti Coen [Tue, 3 Dec 2002 09:18:25 +0000 (09:18 +0000)]
m:exist ==> m:exists

21 years agoFirst implementation of the new generalized SearchPattern on the whole
Claudio Sacerdoti Coen [Mon, 2 Dec 2002 18:18:02 +0000 (18:18 +0000)]
First implementation of the new generalized SearchPattern on the whole
type (not only the conclusion). Despite the file name, no levels have
been implemented so far.

21 years agoBrand new implementation based on functors taking a strategy in input.
Claudio Sacerdoti Coen [Mon, 2 Dec 2002 14:35:13 +0000 (14:35 +0000)]
Brand new implementation based on functors taking a strategy in input.
Several different strategies have been implemented. Unfortunately many
of them are incomparable and there are critical examples where only some
of them terminate in reasonable time.

Removing the functor/module stuff does not bring any sensible performance
improvement even for simple strategies (where most of the functions are
just identity fuctions that can be inlined when not crossing functor
boundaries).