projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2003-01-28
Stefano Zacchiroli
moved tactics in ocaml/tactics
commit
|
commitdiff
|
tree
|
snapshot
2003-01-27
Luca Padovani
* very small fixes here and there
commit
|
commitdiff
|
tree
|
snapshot
2003-01-24
Michele Galatà
Added Decompose tactic
commit
|
commitdiff
|
tree
|
snapshot
2003-01-21
Stefano Zacchiroli
bugfix while printing MutInd and MutConstruct unresolve...
commit
|
commitdiff
|
tree
|
snapshot
2003-01-21
Stefano Zacchiroli
added html templates and pages
commit
|
commitdiff
|
tree
|
snapshot
2003-01-21
Stefano Zacchiroli
- disambiguation implemented!
commit
|
commitdiff
|
tree
|
snapshot
2003-01-21
Stefano Zacchiroli
- added references to gTopLevel needed modules
commit
|
commitdiff
|
tree
|
snapshot
2003-01-21
Claudio Sacerdoti...
New module Disambiguate to hold:
commit
|
commitdiff
|
tree
|
snapshot
2003-01-05
Stefano Zacchiroli
typo: ')' mismatch
commit
|
commitdiff
|
tree
|
snapshot
2002-12-23
Claudio Sacerdoti...
Ambiguous parsing improved: refining is now used to...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-23
Claudio Sacerdoti...
Refine can now also raise Uncertain. The exception...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-23
Claudio Sacerdoti...
The interpretation function can now return also "Implicit".
commit
|
commitdiff
|
tree
|
snapshot
2002-12-22
Claudio Sacerdoti...
New: refinement is now used to disambiguate parsing.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-22
Claudio Sacerdoti...
New constructs \x.T and !x.T introduced. They require...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-22
Claudio Sacerdoti...
* First implementation of CicRefine
commit
|
commitdiff
|
tree
|
snapshot
2002-12-20
Luca Padovani
* if no configuration file is found, issue a warning...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-18
Claudio Sacerdoti...
"Insert Query (Experts only)" menu item added.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-13
Claudio Sacerdoti...
Added a special charcount threatment to the 'append...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-13
Ferruccio Guidi
MathQL textual lexer patched
commit
|
commitdiff
|
tree
|
snapshot
2002-12-13
Claudio Sacerdoti...
Wrong commit undone.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-13
Andrea Asperti
Last commit before major modifications to do.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-13
Michele Galatà
Rearranged tactics in VariousTactics into new modules...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-12
Claudio Sacerdoti...
Minor widget rearrangement.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-12
Claudio Sacerdoti...
notation "@" for append added
commit
|
commitdiff
|
tree
|
snapshot
2002-12-12
Michele Galatà
Added an almost working version of Generalize tactic.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-12
Michele Galatà
Added an almost working version of Generalize tactic.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-12
Michele Galatà
Rearranged tactics in VariousTactics into new modules...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-11
Claudio Sacerdoti...
Severe bug fixed: the test failed in the case of (Rplus...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-11
Claudio Sacerdoti...
* Partial checking of mutual inductive definitions...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-11
Claudio Sacerdoti...
Unary minus now rendered without parentheses.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-10
Claudio Sacerdoti...
"Rewrite ... with ... by ..." line-breaking handled.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-10
Claudio Sacerdoti...
First experimental commit of the notation (partial...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-10
Claudio Sacerdoti...
Ring partially ported to the new library. But I am...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-10
Claudio Sacerdoti...
Bug fixed: beta-redex transformations to LetIn were...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-10
Claudio Sacerdoti...
cut & paste typo fixed
commit
|
commitdiff
|
tree
|
snapshot
2002-12-10
Claudio Sacerdoti...
positive.xsl is now included in headercontent.xsl and...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-09
natile
Now "only" constraint are more restrictive.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-09
Claudio Sacerdoti...
* ElimSimplIntros replace by ElimIntrosSimpl. Simplific...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-09
Claudio Sacerdoti...
* New button "Select only constants" to choose the...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-09
Claudio Sacerdoti...
Simpl now handles let-in reductions as delta-reductions...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
* mQueryLevel2.get_constraints now gives back only...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
New notation for ListSet. It often raises ambiguity...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
instantiate for inductive principles covered
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Andrea Asperti
instantiate for induction principles covered.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
Bug fixed in binary standard MathML Content operators...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
The fresh_name generator has been moved to ProofEngineH...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
Comments removed.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
Bug fixed: when iota-expanding fixpoints the context...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
natile
mQueryLevels2.mli added in Makefile.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
The user interface for the completeSearchPattern query...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
1. depth constraints for Rels and Sorts are now optional
commit
|
commitdiff
|
tree
|
snapshot
2002-12-06
Claudio Sacerdoti...
1. The depth constraint on Rels and Sorts is now optional.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-05
Claudio Sacerdoti...
A simplification bug was introduced during the clean...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-05
Andrea Asperti
Notation for if then else.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-05
Claudio Sacerdoti...
Bug fixed: the lhs part of an explicit name substitutio...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-05
Claudio Sacerdoti...
Minor bug fixes in the 'instantiate' element handling.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Showing a query result which was an inductive type...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Interface improvement: a window is opened to show objec...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
natile
*** empty log message ***
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
New feature: the user can now enter the list of "must...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
* mQueryLevels interface clean-up
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Simplification euristic improved.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Completely broken parsing of Fix and CoFix fixed.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Several bug-fixes to the abstparam hell.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Stefano Zacchiroli
- reverted to only one quotation level for xmluri,...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Variable redefined twice fixed.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
Variable redefined twice fixed.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
New tactic fold_simpl.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-04
Claudio Sacerdoti...
* fold_tac has now a new parameter, which is the reduct...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
Typing of intros_tac improved. It now has a parameter...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
Quick implementation of the "inst" csymbol. It can...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
First working version of the possibility to introduce...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
put_inductive_definition implemented and exposed.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
typecheck_mutual_inductive_defs exposed.
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
An exception was raised when a MutInd or MutConstruct...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Michele Galatà
Added new tactics: Exists, Split, Assumption, Absurd...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-03
Claudio Sacerdoti...
m:exist ==> m:exists
commit
|
commitdiff
|
tree
|
snapshot
2002-12-02
Claudio Sacerdoti...
First implementation of the new generalized SearchPatte...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-02
Claudio Sacerdoti...
Brand new implementation based on functors taking a...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-02
Stefano Zacchiroli
- added a level of quoting on xmluri parameter because...
commit
|
commitdiff
|
tree
|
snapshot
2002-12-02
Andrea Asperti
*** empty log message ***
commit
|
commitdiff
|
tree
|
snapshot
2002-12-01
Enrico Tassi
- now esempi/fourier/ is he dir for all fourier extras
commit
|
commitdiff
|
tree
|
snapshot
2002-11-29
natile
Now MQueryGenerator generates the query and MQueryLevel...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-29
Enrico Tassi
bug in hypotesis parsing solved
commit
|
commitdiff
|
tree
|
snapshot
2002-11-28
Claudio Sacerdoti...
* iff notation added (new csymbol)
commit
|
commitdiff
|
tree
|
snapshot
2002-11-27
Claudio Sacerdoti...
lazily ==> call_by_name (since it is really a call_by_n...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-27
Stefano Zacchiroli
patched Makefile to link also ../gTopLevel/mQueryLevels...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-27
natile
Relation patched, property added.
commit
|
commitdiff
|
tree
|
snapshot
2002-11-27
Claudio Sacerdoti...
* The new query language (now broken) works only on...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-27
Ferruccio Guidi
generator patched
commit
|
commitdiff
|
tree
|
snapshot
2002-11-26
Enrico Tassi
comments in fourier.ml now are in ocamldoc style
commit
|
commitdiff
|
tree
|
snapshot
2002-11-26
Claudio Sacerdoti...
&CSCbr; replaced with 
 to make libxslt stop compl...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-26
Ferruccio Guidi
New module for level management (was in MQueryGenerator)
commit
|
commitdiff
|
tree
|
snapshot
2002-11-26
Ferruccio Guidi
Generator updated for new MathQL.ml
commit
|
commitdiff
|
tree
|
snapshot
2002-11-25
Pietro Di Lena
Changed cic:/Coq/Sets/Ensembles/Ensembles/Empty_set...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-25
Pietro Di Lena
Now it is possible to define a 'cookable' operator...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-22
natile
toplevel.ml patched but it doesn't compile with open...
commit
|
commitdiff
|
tree
|
snapshot
2002-11-22
Stefano Zacchiroli
- use 'query_of_text' to parse textual queries
commit
|
commitdiff
|
tree
|
snapshot
next