]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
we started the implementation of higher order saturated sets
[helm.git] / helm / software / components /
2011-01-20 Wilmer RicciottiBug fix for generation of elimination principles. tree | commitdiff
2011-01-19 Wilmer RicciottiAdded some typing info to elimination principles, allow... tree | commitdiff
2010-12-10 Claudio Sacerdoti... Backporting from new Matita: tree | commitdiff
2010-12-03 Claudio Sacerdoti... Back-portin from new Matita: semantics of ntry changed... tree | commitdiff
2010-12-03 Claudio Sacerdoti... Back-porting from new Matita: improvement to inferred... tree | commitdiff
2010-12-02 Claudio Sacerdoti... Bad default for ?dorefine for instantiate tree | commitdiff
2010-12-02 Claudio Sacerdoti... 1. new implementation of normalize to have a speed... tree | commitdiff
2010-11-29 Claudio Sacerdoti... Bug fixed: propagation of left expected parameters... tree | commitdiff
2010-11-29 Claudio Sacerdoti... In the case type_of constructor with expected type... tree | commitdiff
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita: tree | commitdiff
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita: tree | commitdiff
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita: tree | commitdiff
2010-11-29 Claudio Sacerdoti... Back-porting from new matita: tree | commitdiff
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita: tree | commitdiff
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita: tree | commitdiff
2010-11-23 Claudio Sacerdoti... Debugging code commented out. tree | commitdiff
2010-11-22 Claudio Sacerdoti... Debugging code commented out. tree | commitdiff
2010-11-22 Claudio Sacerdoti... Debugging code commented out. tree | commitdiff
2010-10-19 Enrico Tassicamlp5 probably changed some internal data structures... tree | commitdiff
2010-10-17 Enrico Tassifixed List.for_all2 called without knowing if the two... tree | commitdiff
2010-10-17 Enrico Tassinew case for higher order unification: tree | commitdiff
2010-10-17 Enrico Tassiremoved wrong optimization in delift and export is_flexible tree | commitdiff
2010-09-30 Enrico Tassipatches for hints & unification: tree | commitdiff
2010-09-12 Enrico TassiChange (or better define) the order of hints premises. tree | commitdiff
2010-09-08 Enrico Tassibetter not allowed sort elimination error messsage tree | commitdiff
2010-07-29 Claudio Sacerdoti... Bug fixed: nodes were copied. tree | commitdiff
2010-07-29 Enrico Tassiinterpret non ambiguous symbols ASAP tree | commitdiff
2010-07-28 Enrico Tassi... tree | commitdiff
2010-07-28 Enrico Tassiallows auto before eq is defined tree | commitdiff
2010-07-28 Wilmer RicciottiFixes unexpected behaviour of ncut when multiple goals... tree | commitdiff
2010-07-28 Wilmer RicciottiExperimental enhancements to the ndestruct tactic.... tree | commitdiff
2010-07-22 Enrico Tassido not apply hints if metaclosed tree | commitdiff
2010-07-22 Enrico Tassiavoid assert false, just fail generating the coercion tree | commitdiff
2010-06-17 Enrico Tassioff by one fixed tree | commitdiff
2010-06-10 Wilmer RicciottiFix for inversion principles of types with a single... tree | commitdiff
2010-06-08 Wilmer RicciottiFixed a bug in the undebruijnate function which caused... tree | commitdiff
2010-06-07 Enrico Tassiunify left args of inductive types with left argus... tree | commitdiff
2010-05-12 Wilmer RicciottiExperimental support for Russell (coercions moving... tree | commitdiff
2010-05-10 Enrico Tassinew intro: tree | commitdiff
2010-05-07 Enrico Tassitrace generation with "// by _;" tree | commitdiff
2010-05-06 Claudio Sacerdoti... Bug fixed: nstatus => status (to undo the changes). tree | commitdiff
2010-05-06 Wilmer RicciottiFixing naming scheme for composite coercions. tree | commitdiff
2010-05-06 Claudio Sacerdoti... assert false could happen tree | commitdiff
2010-05-06 Claudio Sacerdoti... Bug fixed: tree | commitdiff
2010-05-04 Wilmer Ricciotti* Fixed a couple of glitches in ndestruct tree | commitdiff
2010-04-19 Andrea AspertiElimination of recursive inductive types leads to looping. tree | commitdiff
2010-04-19 Andrea Aspertialpha_eq instead of pervasives.compare tree | commitdiff
2010-04-13 Enrico Tassifixed makefile tree | commitdiff
2010-04-13 Enrico Tassiauto destructs while introducing in the context tree | commitdiff
2010-04-13 Enrico Tassiprint nobjects (hack with Obj.magic) tree | commitdiff
2010-04-13 Enrico Tassicatch the right exception, avoid uncaught Subst_not_found tree | commitdiff
2010-04-13 Enrico Tassisame heads different arity -> INCOMPARABLE tree | commitdiff
2010-04-13 Enrico Tassisome fixes to THF parser tree | commitdiff
2010-04-11 Ferruccio Guidithe edges must be quoted as well (not only the nodes) tree | commitdiff
2010-04-09 Andrea Aspertiapply_subst_context on statuses tree | commitdiff
2010-04-08 Enrico Tassisupport axioms tree | commitdiff
2010-04-08 Enrico Tassi... tree | commitdiff
2010-04-08 Enrico Tassithf problems list for tptp 4.0.1 tree | commitdiff
2010-04-08 Enrico Tassifixed compiltion order of lexer/parser tree | commitdiff
2010-04-08 Claudio Sacerdoti... New code (unbranched) to compute all keys by all possib... tree | commitdiff
2010-04-08 Claudio Sacerdoti... New sets of. tree | commitdiff
2010-04-08 Enrico TassiTHF parser received some care tree | commitdiff
2010-04-08 Andrea AspertiFixing indexing (commit parziale di Claudio?) tree | commitdiff
2010-04-07 Enrico TassiTHF parser for TPTP tree | commitdiff
2010-03-31 Claudio Sacerdoti... Bug fixed: the current equation is not always the last... tree | commitdiff
2010-03-31 Claudio Sacerdoti... ... tree | commitdiff
2010-03-31 Claudio Sacerdoti... - inversion principles are now generated also for co... tree | commitdiff
2010-03-31 Claudio Sacerdoti... More debugging info from print_tac. tree | commitdiff
2010-03-31 Claudio Sacerdoti... Implicit and UserInput were printed incorrectly. tree | commitdiff
2010-03-31 Andrea AspertiTracing mechanism for auto. Interface changed to solve... tree | commitdiff
2010-03-25 Andrea AspertiExtension of demod to arbtrary predicates (not just... tree | commitdiff
2010-03-24 Claudio Sacerdoti... Equality has one right parameter and thus it's eliminat... tree | commitdiff
2010-03-24 Claudio Sacerdoti... ... tree | commitdiff
2010-03-24 Claudio Sacerdoti... Axioms were not indexed. tree | commitdiff
2010-03-24 Claudio Sacerdoti... Axioms were not indexed. tree | commitdiff
2010-03-24 Claudio Sacerdoti... ... tree | commitdiff
2010-03-24 Andrea AspertiComputation of the trace. tree | commitdiff
2010-03-23 Andrea AspertiFixed a few bugs tree | commitdiff
2010-03-23 Andrea Asperti"flat" function (subst unfolding) tree | commitdiff
2010-03-18 Andrea AspertiPrintings removed. tree | commitdiff
2010-03-18 Andrea AspertiDebugging disabled. tree | commitdiff
2010-03-18 Andrea AspertiDebugging disabled. tree | commitdiff
2010-03-18 Andrea AspertiNew demodulation tactics (mostly for debugging purposes). tree | commitdiff
2010-03-18 Andrea AspertiExporting the demodulation function. tree | commitdiff
2010-03-18 Andrea AspertiNew option "demod" for auto. tree | commitdiff
2010-03-18 Claudio Sacerdoti... Do not index examples (concrete syntax: nremark). tree | commitdiff
2010-03-18 Claudio Sacerdoti... nremark => `Example (not to be indexed) tree | commitdiff
2010-03-18 Andrea Aspertiapp of app inside smart application. tree | commitdiff
2010-03-17 Ferruccio Guididr tree | commitdiff
2010-03-17 Claudio Sacerdoti... OCaml's inferred type simplified. tree | commitdiff
2010-03-17 Claudio Sacerdoti... ... tree | commitdiff
2010-03-16 Claudio Sacerdoti... Comparison of two applications with a different number... tree | commitdiff
2010-03-16 Claudio Sacerdoti... 1) intros cleans up the cache (because the context... tree | commitdiff
2010-03-16 Claudio Sacerdoti... refreshing of inferred type was missing tree | commitdiff
2010-03-12 Andrea AspertiSubst was missing in perforate small (apparently, gty... tree | commitdiff
2010-03-12 Andrea Aspertiremoved debug from the inteface tree | commitdiff
2010-03-04 Andrea AspertiIn line with the ml. tree | commitdiff
2010-03-04 Andrea Asperti1. For smart application, we only perforate small terms... tree | commitdiff
2010-03-04 Andrea AspertiSmall changes for debugging tree | commitdiff
2010-03-04 Andrea AspertiFixed a bug in deep_eq: we generated new clauses but... tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.