| 2008-12-05 |
Claudio Sacerdoti... | Debugging code removed |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging instructions removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | a few missing ~subst added to whd |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | if todo_dom was [] disambiguation was performed twice |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | still commented, but benchmarks the new/old disambiguti... |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | disambiguation takes ~mk_localization_tbl and not ... |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | raise failure instead of uncertain if two terms are... |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | Fixes: |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | housekeeping: |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | Bug fixed: pretty-printing of aliases when the OK butto... |
tree | commitdiff |
| 2008-12-03 |
Claudio Sacerdoti... | The aliases and multi_aliases in the lexicon status... |
tree | commitdiff |
| 2008-12-01 |
Claudio Sacerdoti... | rt.op and check.opt removed from Makefile |
tree | commitdiff |
| 2008-11-30 |
Ferruccio Guidi | lambda-delta/toplevel: improved transformation from... |
tree | commitdiff |
| 2008-11-28 |
Ferruccio Guidi | cicDischarge: final fixup. Now correctly processes... |
tree | commitdiff |
| 2008-11-28 |
Ferruccio Guidi | ng_disambiguation ng_kernel ng_refiner disambiguation... |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | it works! |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | new disambiguator almost attached |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | \forall x:?. and \forall x. both generate a meta for... |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | metas for terms have height 3 |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | New modules stack: |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | cic_disambiguation splitted into disambiguation and... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | disambiguate.ml splitted into disambiguate.ml and cicDi... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | new kernel is compiled since the META of grafite_parser... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | notation now digests Cic.Cast, not sure the precedence... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | disambiguation should not fail if the new refiner fails |
tree | commitdiff |
| 2008-11-26 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-26 |
Enrico Tassi | Re-added exception, just for now (debugging). |
tree | commitdiff |
| 2008-11-26 |
Enrico Tassi | almost done |
tree | commitdiff |
| 2008-11-26 |
Enrico Tassi | disambiguation even more abstracted |
tree | commitdiff |
| 2008-11-25 |
Ferruccio Guidi | cicUtil: we moved here pp_term from proceduralHelpers |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | one more lazy/loc |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | according to camlp5 sources, the dummy loc should be... |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | loc * lazy string -> (loc * string) lazy |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | disambiguation now returns and takes in input the subst... |
tree | commitdiff |
| 2008-11-16 |
Enrico Tassi | removed some printings |
tree | commitdiff |
| 2008-11-16 |
Enrico Tassi | removed some printings |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | missing subst added, now apply rule is probably enough... |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | disambiguation can use a goal as hint for the expected... |
tree | commitdiff |
| 2008-11-14 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | disambiguation for ng terms almost there |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | some new exports |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | new meta added for ng_disambiguation |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | exported disambiguate_thing |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | occurr check fixed |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | more printings |
tree | commitdiff |
| 2008-11-07 |
Andrea Asperti | debug=false |
tree | commitdiff |
| 2008-11-07 |
Andrea Asperti | Signature_of has been closed with respect to constructors. |
tree | commitdiff |
| 2008-11-07 |
Andrea Asperti | The signature in "retrieve equations" must be extended... |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | do not erase sorts |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | better error messages. sorts are compared using whd |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | Evil case fixed, the coulde should be more readable |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | removed empty lines |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | the passive set and passive list are expected to have... |
tree | commitdiff |
| 2008-11-05 |
Enrico Tassi | new internal flags for auto: |
tree | commitdiff |
| 2008-11-05 |
Enrico Tassi | duplicate entry in menv avoided |
tree | commitdiff |
| 2008-11-04 |
Andrea Asperti | Calling unification instead of matching when checking... |
tree | commitdiff |
| 2008-11-03 |
Enrico Tassi | removed prerr_endline |
tree | commitdiff |
| 2008-11-03 |
Enrico Tassi | debug=false |
tree | commitdiff |
| 2008-11-01 |
Enrico Tassi | added lazy |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Propagation of changes in paramodulation. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Exported a couple of functions. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Added a in_universe function |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | propagation of changes in other paramodulation files. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | New demod function working for arbitary goals. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Enforcing the disjoint invariant between metasenvs. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Main change: added a parameter to build_equality_proof... |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | many bugs fixed |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | metasenv passed to get_relevance, Metas that stand... |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | _ in place of unused variables |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | Implicit annotationas are now printed |
tree | commitdiff |
| 2008-10-22 |
Ferruccio Guidi | we aligned the implementation to the plmms08 paper |
tree | commitdiff |
| 2008-10-21 |
Enrico Tassi | better pps |
tree | commitdiff |
| 2008-10-21 |
Enrico Tassi | - mk_restricted_irl removed, the non-optimized code... |
tree | commitdiff |
| 2008-10-21 |
Enrico Tassi | psubst for metas fixed again |
tree | commitdiff |
| 2008-10-20 |
Enrico Tassi | more bug fixed (or introduced) |
tree | commitdiff |
| 2008-10-20 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-10-18 |
Ferruccio Guidi | Acic2Procedural: |
tree | commitdiff |
| 2008-10-17 |
Enrico Tassi | new command eval added |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | delifting a Meta with an IRL w.r.t. another IRL complet... |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | some bug fixed |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | subst_meta was missing |
tree | commitdiff |
| 2008-10-14 |
Enrico Tassi | more work |
tree | commitdiff |
| 2008-10-14 |
Enrico Tassi | term refinement almost done, some functions exported... |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | initial refiner .... |
tree | commitdiff |
| 2008-10-13 |
Claudio Sacerdoti... | Bug fixed in LetIn: the cumulativity test was performed... |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | bug in psubst fixed inside local context in Irl form |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | better error message |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | ppmetasenv & subst added |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | NCicReduction.reduce_machine returns a boolean stating... |
tree | commitdiff |
| next |
projects / helm.git / history