| 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 |
| 2002-11-22 |
Stefano Zacchiroli | - catch processing exception which are now reported... |
commit | commitdiff | tree | snapshot |
| 2002-11-22 |
Stefano Zacchiroli | - first (draft) version of searchEngine |
commit | commitdiff | tree | snapshot |
| 2002-11-21 |
Claudio Sacerdoti... | WARNING!!! |
commit | commitdiff | tree | snapshot |
| 2002-11-21 |
Claudio Sacerdoti... | Some stylesheets are now generated with Di Lena's meta_... |
commit | commitdiff | tree | snapshot |
| 2002-11-21 |
Pietro Di Lena | Porting to the new DTD for MoWGLI. |
commit | commitdiff | tree | snapshot |
| 2002-11-21 |
no author | This commit was manufactured by cvs2svn to create branch |
commit | commitdiff | tree | snapshot |
| 2002-11-20 |
Enrico Tassi | - removed: cut_tac False to demostrate False |
commit | commitdiff | tree | snapshot |
| 2002-11-19 |
Claudio Sacerdoti... | ~ask_dtd_to_the_getter parameter added to Cic2Xml.print... |
commit | commitdiff | tree | snapshot |
| 2002-11-19 |
Claudio Sacerdoti... | Param ~ask_dtd_to_the_getter added to Cic2Xml.print_object. |
commit | commitdiff | tree | snapshot |
| 2002-11-19 |
Claudio Sacerdoti... | Big change: Qed saves the theorem/definition and regist... |
commit | commitdiff | tree | snapshot |
| 2002-11-19 |
Claudio Sacerdoti... | innertypesuri_of_uri implemented |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Interface improvement (???): the Check button has been... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Small interface improvement: the menu is now in an... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Interface improvement: |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Code clean-up: the widget in the lower-left corner... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Aliases definition removed from the CIC textual parser. |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Aliases definition removed from the |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Inteface improvement: the "Edit Aliases..." menu entry... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Major interface improvements. |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Rendering of InductiveDefinitions, Variables and Axioms... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | URLs_or_URIs param added to choose if the xlink:href... |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | Identifier added to inductiveType in the DTD. |
commit | commitdiff | tree | snapshot |
| 2002-11-18 |
Claudio Sacerdoti... | IllFormedUri exception now exported. |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Order of the generated metavariables for apply fixed... |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Comments improved. |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Bug fixed: conjectures were printed in the wrong order. |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Metasenv partially checked. |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | * Bug fixed: a real empty page is now really used for... |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Residual interface bug fixes: no sequent page is now... |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Small interface improvement: the first goal page is... |
commit | commitdiff | tree | snapshot |
| 2002-11-15 |
Claudio Sacerdoti... | Small interface improvements. |
commit | commitdiff | tree | snapshot |
| 2002-11-14 |
Claudio Sacerdoti... | Other small improvements to the general window layout. |
commit | commitdiff | tree | snapshot |
| 2002-11-14 |
Stefano Zacchiroli | name fixes due to changes in libhttp-ocaml (e.g. s... |
commit | commitdiff | tree | snapshot |
| 2002-11-14 |
Claudio Sacerdoti... | Default for the reduction moved to CicReductionMachine. |
commit | commitdiff | tree | snapshot |
| 2002-11-14 |
Claudio Sacerdoti... | Small interface improvement: selecting something in... |
commit | commitdiff | tree | snapshot |
| 2002-11-14 |
Claudio Sacerdoti... | Interface improvement: |
commit | commitdiff | tree | snapshot |
| 2002-11-13 |
Claudio Sacerdoti... | Interface improvements: the window to disambiguate... |
commit | commitdiff | tree | snapshot |
| 2002-11-13 |
Stefano Zacchiroli | switched to OCaml HTTP module |
commit | commitdiff | tree | snapshot |
| 2002-11-13 |
Matteo Selmi | Written instantiate for content level |
commit | commitdiff | tree | snapshot |
| 2002-11-12 |
Claudio Sacerdoti... | A frame now surrounds the XMHTML widget. |
commit | commitdiff | tree | snapshot |
| 2002-11-12 |
Stefano Zacchiroli | symlink automagically cicReduction.ml if it doesn't... |
commit | commitdiff | tree | snapshot |
| 2002-11-12 |
Claudio Sacerdoti... | Heavy restyling of the interface. |
commit | commitdiff | tree | snapshot |
| 2002-11-11 |
Enrico Tassi | An old bug in 'eqT' hipotesys solved |
commit | commitdiff | tree | snapshot |
| 2002-11-06 |
Matteo Selmi | Modified mode "abstparam" due to changes to LAMBDA... |
commit | commitdiff | tree | snapshot |
| 2002-11-06 |
Claudio Sacerdoti... | - big interface changes: open goals are now collected... |
commit | commitdiff | tree | snapshot |
| 2002-11-05 |
Claudio Sacerdoti... | mathql_interpreter_galax removed |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | Quick fix to view metadata theories again. The case... |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | nameObject ==> objectName |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | The reduction tactics are now shared between ReductionT... |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | The fold tactic of proofEngine now uses ReductionTactic... |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | - Comments updated |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | - synchronization with the main branch |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | - porting to the new theory with explicit named substit... |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | - new fold tactic |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | - new CicTextualParser |
commit | commitdiff | tree | snapshot |
| 2002-11-04 |
Claudio Sacerdoti... | New CicTextualParser: it now returns (approximately... |
commit | commitdiff | tree | snapshot |
| 2002-11-02 |
Matteo Selmi | Corrected some wrong paths |
commit | commitdiff | tree | snapshot |
| 2002-11-02 |
Matteo Selmi | Corrected some wrong paths |
commit | commitdiff | tree | snapshot |
| 2002-10-31 |
Claudio Sacerdoti... | Several bug-fixes: |
commit | commitdiff | tree | snapshot |
| 2002-10-31 |
Claudio Sacerdoti... | Bug fixed: the declared number of new goals of Apply... |
commit | commitdiff | tree | snapshot |
| 2002-10-31 |
Claudio Sacerdoti... | Better layout of the buttons. |
commit | commitdiff | tree | snapshot |
| 2002-10-31 |
Michele Galatà | Added variousTactic with Constructor, Left, Right,... |
commit | commitdiff | tree | snapshot |
| 2002-10-31 |
Claudio Sacerdoti... | - ElimIntrosSimpl now implemented using tacticals.... |
commit | commitdiff | tree | snapshot |
| 2002-10-31 |
Claudio Sacerdoti... | explicit namd substitutions introduced |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog