| 2007-05-09 |
Andrea Asperti | A few extensions for the moebius inversion theorem
|
commit | commitdiff | tree |
| 2007-05-09 |
Andrea Asperti | Proof of the moebius inversion theorem
|
commit | commitdiff | tree |
| 2007-04-30 |
Andrea Asperti | Even if we are at depth 0, we first check in the cache...
|
commit | commitdiff | tree |
| 2007-04-30 |
Andrea Asperti | Removed an assert false; everything works again, but...
|
commit | commitdiff | tree |
| 2007-04-27 |
Andrea Asperti | Subst is passed in input to apapluy, so no need to...
|
commit | commitdiff | tree |
| 2007-04-27 |
Andrea Asperti | Apply_with_subst now returns a subst with a correct...
|
commit | commitdiff | tree |
| 2007-04-24 |
Andrea Asperti | Subsumption_subst re-added to initial.
|
commit | commitdiff | tree |
| 2007-04-24 |
Andrea Asperti | @
|
commit | commitdiff | tree |
| 2007-03-16 |
Andrea Asperti | New contrib moebius.ma.
|
commit | commitdiff | tree |
| 2007-03-16 |
Andrea Asperti | Extensions required for the moebius function (in Z).
|
commit | commitdiff | tree |
| 2007-03-13 |
Andrea Asperti | Few theorems added.`
|
commit | commitdiff | tree |
| 2007-03-13 |
Andrea Asperti | new version of div_and_mod
|
commit | commitdiff | tree |
| 2007-03-13 |
Andrea Asperti | Capturing Invalid_argument inside pp (otherwise we...
|
commit | commitdiff | tree |
| 2007-01-16 |
Andrea Asperti | Added SetoidInc.m
|
commit | commitdiff | tree |
| 2007-01-16 |
Andrea Asperti | Some CoRN files.
|
commit | commitdiff | tree |
| 2006-12-22 |
Andrea Asperti | Add_moo_content modified to avoid repetitions of index...
|
commit | commitdiff | tree |
| 2006-12-22 |
Andrea Asperti | Minor change.
|
commit | commitdiff | tree |
| 2006-12-22 |
Andrea Asperti | Collapse_head_metas transforms all terms "not-recongnized...
|
commit | commitdiff | tree |
| 2006-12-22 |
Andrea Asperti | In the let-in case we compute the type and add it to...
|
commit | commitdiff | tree |
| 2006-12-22 |
Andrea Asperti | The function uri_of_term now works also if the explciit...
|
commit | commitdiff | tree |
| 2006-12-18 |
Andrea Asperti | M logic/coimplication.ma
|
commit | commitdiff | tree |
| 2006-12-18 |
Andrea Asperti | Renamed iterative into map_iter_p and moved around...
|
commit | commitdiff | tree |
| 2006-12-18 |
Andrea Asperti | Proof of Euler theorem.
|
commit | commitdiff | tree |
| 2006-11-29 |
Andrea Asperti | Demodulate_tac now depends on the universe
|
commit | commitdiff | tree |
| 2006-11-28 |
Andrea Asperti | Changed an ahstable into an association list.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Added in_eq_uris.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Fix_proof should recursively work on explicit substs.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Removed a couple of assertions.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Commented an assertion.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Commented an assertion.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Commented a few assertions.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Variant are not indexed.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Only modified for taking unfold into account.
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Matita's default equality has changed
|
commit | commitdiff | tree |
| 2006-11-27 |
Andrea Asperti | Small changes
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Command index added to disambiguate.
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Added a new command "index" for the indexing terms...
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Set of Set of uri added.
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Modifications to auto due to the introduction of the...
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Universe is a discrimination-tree structure.
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | The status has been extended with a "universe", that...
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Fixed a call to auto, and commented the remaining part.
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | paramodulation removed
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Minor changes.
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Simplified version.
|
commit | commitdiff | tree |
| 2006-11-23 |
Andrea Asperti | Adding CoRN.
|
commit | commitdiff | tree |
| 2006-11-15 |
Andrea Asperti | lt_O_S moved to nat/orders.ma
|
commit | commitdiff | tree |
| 2006-11-15 |
Andrea Asperti | Added lt_O_S.
|
commit | commitdiff | tree |
| 2006-10-30 |
Andrea Asperti | library = yes!
|
commit | commitdiff | tree |
| 2006-10-25 |
Andrea Asperti | Added a couple of flags to auto
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | Demodulate and applyS moved form saturation to auto.
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | Major changes to auto, documented on the helm mailing...
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | Minor changes.
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | a. uniform mangement for context and library
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | The type of universe_of_goals has slightly changed...
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | This is only a temporary patch. The typecheker raises a
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | The function exists_a_meta has been modified to capture...
|
commit | commitdiff | tree |
| 2006-10-20 |
Andrea Asperti | New function pack_coercion_metasenv, used in auto after...
|
commit | commitdiff | tree |
| 2006-10-09 |
Andrea Asperti | Theorems from the library and from the context are...
|
commit | commitdiff | tree |
| 2006-10-09 |
Andrea Asperti | The two coercions sym_eq e eq_f gives BIG TROUBLES...
|
commit | commitdiff | tree |
| 2006-10-09 |
Andrea Asperti | Factorized "find_equalities" in demodulation_tac.
|
commit | commitdiff | tree |
| 2006-10-03 |
Andrea Asperti | New home page, with italian version.
|
commit | commitdiff | tree |
| 2006-10-03 |
Andrea Asperti | Changed auto from implicit to option and renamed a...
|
commit | commitdiff | tree |
| 2006-09-04 |
Andrea Asperti | Generation of inductive and inversion principles for...
|
commit | commitdiff | tree |
| 2006-09-04 |
Andrea Asperti | Bug fixing. If the inductive types do not occur in...
|
commit | commitdiff | tree |
| 2006-07-24 |
Andrea Asperti | Bug fixed: a symbol alias Symb(s,0) now subsumes the...
|
commit | commitdiff | tree |
| 2006-07-24 |
Andrea Asperti | A compiling version of the library.
|
commit | commitdiff | tree |
| 2006-07-14 |
Andrea Asperti | Added the computation of max_weight.
|
commit | commitdiff | tree |
| 2006-07-14 |
Andrea Asperti | Added the computation of max_weight for equations in...
|
commit | commitdiff | tree |
| 2006-06-29 |
Andrea Asperti | Cleaning up; removed a couple of "open".
|
commit | commitdiff | tree |
| 2006-06-19 |
Andrea Asperti | some experiments
|
commit | commitdiff | tree |
| 2006-06-19 |
Andrea Asperti | added (but still unused) remove_local_context
|
commit | commitdiff | tree |
| 2006-06-19 |
Andrea Asperti | added (but not yet used) remove_local_context
|
commit | commitdiff | tree |
| 2006-06-19 |
Andrea Asperti | Utils.compare_terms instead of compare_weights
|
commit | commitdiff | tree |
| 2006-06-19 |
Andrea Asperti | occur_check and unification fixed. now Meta(i,[]) and...
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | some examples of the new ApplyS tactic
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | examples of applyS
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | Apply-Silvie tactic added!
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | added applyS
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | some fixed done in Orsay:
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | exported 2 functions needed by applyS
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | ...
|
commit | commitdiff | tree |
| 2006-06-15 |
Andrea Asperti | default constants are now the matita standard library...
|
commit | commitdiff | tree |
| 2006-06-09 |
Andrea Asperti | Notation for congruent.
|
commit | commitdiff | tree |
| 2006-06-01 |
Andrea Asperti | Subsumption_subst must be applied to the initial proof...
|
commit | commitdiff | tree |
| 2006-05-26 |
Andrea Asperti | 1) variables occurring only in proofs anre not relocated
|
commit | commitdiff | tree |
| 2006-05-26 |
Andrea Asperti | Bug fixed: the syntax "?n" used to be broken. It tried...
|
commit | commitdiff | tree |
| 2006-05-23 |
Andrea Asperti | added important comment
|
commit | commitdiff | tree |
| 2006-05-23 |
Andrea Asperti | fixed LetIn proofs
|
commit | commitdiff | tree |
| 2006-05-23 |
Andrea Asperti | added stuff for profiling macros
|
commit | commitdiff | tree |
| 2006-05-05 |
Andrea Asperti | New version of deep_subsumption
|
commit | commitdiff | tree |
| 2006-04-27 |
Andrea Asperti | Equality chains.
|
commit | commitdiff | tree |
| 2006-04-27 |
Andrea Asperti | Added is_trans_eq_URI and is_sym_eq_URI
|
commit | commitdiff | tree |
| 2006-04-26 |
Andrea Asperti | Build_proof_goal does not return the metasenv any more.
|
commit | commitdiff | tree |
| 2006-04-26 |
Andrea Asperti | fixed demodulation_goal (used to return always false)
|
commit | commitdiff | tree |
| 2006-04-26 |
Andrea Asperti | removed ocaml equality on equations
|
commit | commitdiff | tree |
| 2006-04-10 |
Andrea Asperti | Removed negative equations.
|
commit | commitdiff | tree |
| 2006-04-04 |
Andrea Asperti | Naif substitution. Removed local context in metas during...
|
commit | commitdiff | tree |
| 2006-03-27 |
Andrea Asperti | args removed from equalities.
|
commit | commitdiff | tree |
| 2006-03-24 |
Andrea Asperti | New unification and new matching.
|
commit | commitdiff | tree |
| next |
projects / helm.git / search