projects / helm.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
helm.git
2009-06-08 Enrico Tassisome more functors and a nice higher-order all_position... commit | commitdiff | tree | snapshot
2009-06-08 Enrico Tassiadded META for ng_paramodulation commit | commitdiff | tree | snapshot
2009-06-06 Claudio Sacerdoti... Previous commit reverted, as explained in that log. commit | commitdiff | tree | snapshot
2009-06-06 Claudio Sacerdoti... This commit restores the ids_to_father_ids table. commit | commitdiff | tree | snapshot
2009-06-06 Enrico Tassisome renaming to make ocamlopt happy commit | commitdiff | tree | snapshot
2009-06-05 Ferruccio Guidibugfix in Include syntax: it was changed and committed... commit | commitdiff | tree | snapshot
2009-06-05 Ferruccio Guidi- Procedural convertible rewrites in the conclusion... commit | commitdiff | tree | snapshot
2009-06-05 denesFirst tests for paramodulation (pretty printer, unifica... commit | commitdiff | tree | snapshot
2009-06-05 Wilmer Ricciotti- replaced part1a/defn with the version based on induct... commit | commitdiff | tree | snapshot
2009-06-05 denesFix : wrong exception was catch in apply_subst commit | commitdiff | tree | snapshot
2009-06-05 Claudio Sacerdoti... 1) the home button of CicBrowser now works also for NG commit | commitdiff | tree | snapshot
2009-06-05 Claudio Sacerdoti... The kernel _must_ check the correctness of the height... commit | commitdiff | tree | snapshot
2009-06-04 Ferruccio Guidisyntax error fixed :( commit | commitdiff | tree | snapshot
2009-06-04 Ferruccio Guidi- doubleTypeInference: we check for unreferenced letins... commit | commitdiff | tree | snapshot
2009-06-04 denesFirst pretty printing functions commit | commitdiff | tree | snapshot
2009-06-04 Enrico Tassiminor changes here and there. We extend fo-unification... commit | commitdiff | tree | snapshot
2009-06-04 Enrico Tassicomments commit | commitdiff | tree | snapshot
2009-06-04 Enrico Tassibetter type for comparison and implementation of KBO... commit | commitdiff | tree | snapshot
2009-06-04 Enrico Tassimore functors commit | commitdiff | tree | snapshot
2009-06-03 Ferruccio Guidi- boxPp: added missing spaces commit | commitdiff | tree | snapshot
2009-06-03 Wilmer RicciottiUpdate, using induction/inversion. commit | commitdiff | tree | snapshot
2009-06-03 Enrico Tassifunctorial abstraction over term blobs commit | commitdiff | tree | snapshot
2009-06-03 Andrea Aspertinot_to_not commit | commitdiff | tree | snapshot
2009-06-03 Claudio Sacerdoti... New test for NG notation. commit | commitdiff | tree | snapshot
2009-06-03 Claudio Sacerdoti... Huge commit with several changes: commit | commitdiff | tree | snapshot
2009-06-01 denesFirst implementation of unification on foterms commit | commitdiff | tree | snapshot
2009-06-01 denesFirst functions on substitutions for unification commit | commitdiff | tree | snapshot
2009-06-01 Enrico Tassiadded a snapshot of comparison commit | commitdiff | tree | snapshot
2009-06-01 Andrea AspertiThis works for me commit | commitdiff | tree | snapshot
2009-06-01 Enrico Tassiwe rewrite the paramodulation code! commit | commitdiff | tree | snapshot
2009-05-29 Wilmer RicciottiPOPLmark part 1a using the de Bruijn encoding. commit | commitdiff | tree | snapshot
2009-05-29 Ferruccio Guidi- cicNotationParser: added extra space to TeX control... commit | commitdiff | tree | snapshot
2009-05-28 Ferruccio GuidiProcedural: higher-order unification needs a lot of... commit | commitdiff | tree | snapshot
2009-05-28 Ferruccio Guidi- cicInspect: relevant nodes count updated: letin nodes... commit | commitdiff | tree | snapshot
2009-05-27 Ferruccio GuidiProcedural: bugfix in the generation of intros for... commit | commitdiff | tree | snapshot
2009-05-27 Ferruccio Guidi- Procedural: we specify more unifiers for apply to... commit | commitdiff | tree | snapshot
2009-05-27 Claudio Sacerdoti... Basic support for interpretations for NG: commit | commitdiff | tree | snapshot
2009-05-27 Andrea AspertiAvoiding to filter the application of congruence equations commit | commitdiff | tree | snapshot
2009-05-26 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-05-26 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-05-26 Andrea Aspertiremoved a call to autobatch. commit | commitdiff | tree | snapshot
2009-05-25 Enrico Tassinasty change in the lexer/parser: commit | commitdiff | tree | snapshot
2009-05-22 Ferruccio Guidibugfix in the output notation for eq commit | commitdiff | tree | snapshot
2009-05-22 Andrea AspertiPruning candidates in the applicative case for equalities. commit | commitdiff | tree | snapshot
2009-05-21 Ferruccio GuidiProcedural: we use the expected type rather than the... commit | commitdiff | tree | snapshot
2009-05-21 Ferruccio Guidi- cicUtil: is_sober now detects non-positive rels. commit | commitdiff | tree | snapshot
2009-05-21 Andrea Aspertiautobatch -> autobatch by commit | commitdiff | tree | snapshot
2009-05-20 Ferruccio Guidiwe catch the refiner errors in the critical step and... commit | commitdiff | tree | snapshot
2009-05-20 Andrea AspertiRemoved a silly type check commit | commitdiff | tree | snapshot
2009-05-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2009-05-19 Andrea AspertiNotEq is now considered as a negative Eq atom commit | commitdiff | tree | snapshot
2009-05-19 Enrico Tassiregenerated commit | commitdiff | tree | snapshot
2009-05-19 Enrico Tassifixed generation of horn clauses, negated atoms are... commit | commitdiff | tree | snapshot
2009-05-19 Enrico Tassisome horn+equality problems commit | commitdiff | tree | snapshot
2009-05-18 Claudio Sacerdoti... removed byte queries commit | commitdiff | tree | snapshot
2009-05-18 Enrico Tassiremoved useless function commit | commitdiff | tree | snapshot
2009-05-18 Enrico Tassiin the new kernel you can type Type[i] to mean Type_i... commit | commitdiff | tree | snapshot
2009-05-18 Enrico Tassinothing special commit | commitdiff | tree | snapshot
2009-05-18 Claudio Sacerdoti... 1) GrafiteAst.NEval => GrafiteAst.NReduce commit | commitdiff | tree | snapshot
2009-05-18 Claudio Sacerdoti... 1) new tactic normalize (low-level function implemented in commit | commitdiff | tree | snapshot
2009-05-18 Claudio Sacerdoti... 1) order of processing of case branches reverted (to... commit | commitdiff | tree | snapshot
2009-05-17 Claudio Sacerdoti... maxmeta implemented commit | commitdiff | tree | snapshot
2009-05-17 Claudio Sacerdoti... maxmeta function to return the heighest meta used so far commit | commitdiff | tree | snapshot
2009-05-17 Claudio Sacerdoti... alpha_eq exported commit | commitdiff | tree | snapshot
2009-05-17 Claudio Sacerdoti... alpha_eq defined and exported commit | commitdiff | tree | snapshot
2009-05-17 Claudio Sacerdoti... efficiency improvement (buffers are now used everywhere) commit | commitdiff | tree | snapshot
2009-05-17 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-05-17 Enrico Tassibyte tests disabled commit | commitdiff | tree | snapshot
2009-05-15 Enrico Tassiadded patch to not unify any term containing the in_sco... commit | commitdiff | tree | snapshot
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth... commit | commitdiff | tree | snapshot
2009-05-15 Claudio Sacerdoti... Cosmetic. commit | commitdiff | tree | snapshot
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth commit | commitdiff | tree | snapshot
2009-05-14 Ferruccio Guidi- libraryObjects: new default "natural numbers" with... commit | commitdiff | tree | snapshot
2009-05-13 Ferruccio Guidiinterpretations placed right after the corresponding... commit | commitdiff | tree | snapshot
2009-05-13 Ferruccio Guidi- matitaEngine: some commands like "coercion" must... commit | commitdiff | tree | snapshot
2009-05-13 Andrea AspertiThe singature of the "by" universe is added to the... commit | commitdiff | tree | snapshot
2009-05-13 Andrea AspertiVia un'altra linea... commit | commitdiff | tree | snapshot
2009-05-13 Andrea AspertiSempre piu' breve commit | commitdiff | tree | snapshot
2009-05-13 Andrea AspertiSignature is computed on the initial goal, once and... commit | commitdiff | tree | snapshot
2009-05-12 Claudio Sacerdoti... Do we really want to generate eliminators for nested... commit | commitdiff | tree | snapshot
2009-05-12 Claudio Sacerdoti... All weakly positive types but imbricated ones are now... commit | commitdiff | tree | snapshot
2009-05-12 Ferruccio Guidi- Procedural: we now reconstruct "let H := v in t"... commit | commitdiff | tree | snapshot
2009-05-12 Andrea AspertiWe only filter the smart candidates w.r.t the signature commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... Some experiments in generation of elimination principles. commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... ppsubst commented out in ppobj commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... Bug fixed: the relevance list can be shorted then leftn... commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... Missing spaces inserted here and there. commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... - non_punctuational_tacticals ported to NG commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... Buffers are now used everywhere for speed-up. commit | commitdiff | tree | snapshot
2009-05-11 Claudio Sacerdoti... New function list_iter_sep. commit | commitdiff | tree | snapshot
2009-05-11 Andrea AspertiA few lemmas about inclusion. commit | commitdiff | tree | snapshot
2009-05-11 Andrea AspertiMore automation commit | commitdiff | tree | snapshot
2009-05-10 Claudio Sacerdoti... - critical bug fixed in NCicSubstitution.lift: commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... Stupid typing error fixed. commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... Bug fixed: left parameters of constructors were unified... commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... Bug fixed: refinement of mutual recursive definitions... commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... Improved tests (for left parameters and mutual recursiv... commit | commitdiff | tree | snapshot
2009-05-08 Claudio Sacerdoti... Bug fixed in refinement of inductive types: left parame... commit | commitdiff | tree | snapshot
next
Unnamed repository; edit this file 'description' to name the repository.