]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_disambiguation
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_disambiguation /
2005-11-22 Claudio Sacerdoti... Less verbose error messages.
2005-11-19 Claudio Sacerdoti... "let rec f = ... in f l" used to be compiled incorrectly
2005-11-19 Claudio Sacerdoti... Less verbose error messages (= substitution applied...
2005-11-19 Claudio Sacerdoti... Wrong reported error message fixed.
2005-11-19 Claudio Sacerdoti... More information is now printed when reporting errors.
2005-11-19 Claudio Sacerdoti... Typo fixed.
2005-11-19 Claudio Sacerdoti... Disambiguation errors are no longer thrown away. They...
2005-11-08 Claudio Sacerdoti... Debugging code removed.
2005-11-07 Claudio Sacerdoti... Avoid generation of let x = let rec x = ... in x in...
2005-11-07 Claudio Sacerdoti... Duplicated exception definition removed (used to give...
2005-10-25 Enrico Tassimoved the expansion of implicits inside the refiner...
2005-10-25 Claudio Sacerdoti... Every exception that used to have type string is now...
2005-10-05 Stefano Zacchirolis/commands_of_domain_and_codomain_items_list/aliases_of...
2005-10-05 Stefano Zacchirolirebuilt
2005-09-29 Claudio Sacerdoti... Further speed-up in the disambiguation algorithm.
2005-09-23 Claudio Sacerdoti... New module HMysql (to abstract over Mysql and make...
2005-09-23 Claudio Sacerdoti... CicUtil.profile ==> HExtlib.profile
2005-09-23 Enrico Tassiadded universes
2005-09-23 Claudio Sacerdoti... The disambiguation now returns the aliases diff. It...
2005-09-23 Claudio Sacerdoti... Environment replaced by lists of domain and codomain...
2005-09-21 Claudio Sacerdoti... This commit removes the slowest identity function ever...
2005-09-21 Stefano Zacchiroliported to the new parser interface (Ulexing.lexbuf...
2005-09-21 Claudio Sacerdoti... 1. profiling code added
2005-09-19 Claudio Sacerdoti... This commit (partially) removes a big source of ineffic...
2005-09-15 Claudio Sacerdoti... Yet another implementation of the single aliases /...
2005-09-14 Stefano Zacchiroliadded hyperlinks on case pattern heads and outtype
2005-09-13 Stefano Zacchiroliadded "commands_of_environment"
2005-09-13 Stefano Zacchiroliregenerated
2005-09-13 Stefano Zacchirolimoved dummy_floc from Disambiguate to DisambiguateTypes...
2005-09-12 Stefano Zacchirolicic_textual_parser2 -> cic_disambiguation
2005-09-12 Stefano Zacchiroliremoved debugging print
2005-09-12 Stefano Zacchiroliadded support for multi-aliases in disambiguation envir...
2005-09-08 Stefano Zacchiroliimplemented lazy disambiguation of tactics arguments...
2005-08-30 Claudio Sacerdoti... A parser for aliases implemented (required by the Whelp).
2005-07-26 Claudio Sacerdoti... **** Experimental: ****
2005-07-20 Claudio Sacerdoti... Pretty printing of the disambiguation environment no...
2005-07-18 Stefano Zacchiroli- removed old parser
2005-07-18 Stefano Zacchirolimerged cic_notation with disambiguation: good luck!
2005-07-11 Claudio Sacerdoti... Bug fixed: the left parameters of a record or inductive...
2005-07-08 Enrico Tassiadded Variant theorem flavour
2005-07-07 Claudio Sacerdoti... Bug fixed: uris can contain '-' (e.g. cic:/Sophia-Antip...
2005-07-06 Claudio Sacerdoti... 1. tactical "try_tacticals" renamed to "first"
2005-07-06 Claudio Sacerdoti... * Bug fixed: "tac." was parsed as Seq [tac]
2005-07-05 Ferruccio Guidiname specifications added for elim_intros, elim_intros_...
2005-07-05 Claudio Sacerdoti... Debugging back to false
2005-07-05 Claudio Sacerdoti... Bug fixed: the outtype of a match when omitted was...
2005-07-04 Claudio Sacerdoti... New command default "foo" uri1 ... urin
2005-07-04 Claudio Sacerdoti... "include" command implemented.
2005-07-01 Enrico Tassion is now a keyword (needed in let rec)
2005-07-01 Claudio Sacerdoti... TacticAst2Box no longer used.
2005-07-01 Claudio Sacerdoti... Syntax of patterns changed again to make it non-ambiguous:
2005-06-30 Claudio Sacerdoti... The pattern of a fold cannot have the "wanted" part...
2005-06-30 Claudio Sacerdoti... Signature and concrete syntax of fold fixed.
2005-06-30 Ferruccio Guidilapply and fwd improved
2005-06-30 Claudio Sacerdoti... 1. rewrite_* and rewrite_back_* merged into one function
2005-06-29 Claudio Sacerdoti... 1. new syntax for patterns:
2005-06-28 Enrico Tassiadded Drop
2005-06-28 Claudio Sacerdoti... New argument for LApply: the ident for the generated...
2005-06-27 Claudio Sacerdoti... A few other tactics made available to matita.
2005-06-27 Claudio Sacerdoti... New argument (the identifier) to generalize.
2005-06-27 Claudio Sacerdoti... New argument (the hypothesis name) for cut.
2005-06-27 Enrico Tassisupport for _ in binders, and a more coplex pattern...
2005-06-27 Claudio Sacerdoti... More tactics or tactic arguments made available to...
2005-06-27 Claudio Sacerdoti... More tactics are now available to matita.
2005-06-27 Enrico Tassifixed LApply pretty printing
2005-06-25 Ferruccio Guidifirs wrking (?) version of lapply
2005-06-24 Claudio Sacerdoti... Asts generalized: a lot of tactics where restricted...
2005-06-23 Claudio Sacerdoti... The discriminate tactic accepts a term, not only an...
2005-06-23 Claudio Sacerdoti... 1 .Tactic generalize ported to patterns and activated...
2005-06-17 Enrico Tassiconcrete syntax for goal patterns
2005-06-17 Claudio Sacerdoti... more strings to UriManager.uri
2005-06-17 Claudio Sacerdoti... many strings that are supposed to be URIs are now UriMa...
2005-06-15 Claudio Sacerdoti... The `Record class now records also the name of the...
2005-06-15 Claudio Sacerdoti... Bug fixed: parsing errors were ignored by matitac since...
2005-06-15 Ferruccio Guidibeginning of the tactics lapply and fwd
2005-06-15 Claudio Sacerdoti... Big commit and major code clean-up:
2005-06-14 Claudio Sacerdoti... * no more %% comments
2005-06-14 Claudio Sacerdoti... parentheses allowed inside comments
2005-06-14 Claudio Sacerdoti... test_lexer and test_parser compiled by default
2005-06-14 Enrico Tassiremoved ocaml-pxp
2005-06-10 Enrico Tassiadded records
2005-06-10 Claudio Sacerdoti... The type of the left parameters of an inductive type...
2005-06-10 Claudio Sacerdoti... The user is no longer obliged to give the types for...
2005-06-10 Claudio Sacerdoti... More debugging infos.
2005-06-08 Claudio Sacerdoti... The type of a top-level "let rec" can be optional.
2005-06-08 Claudio Sacerdoti... New syntax (again) for let rec binders:
2005-06-08 Claudio Sacerdoti... New lighter syntax for "let rec".
2005-06-08 Claudio Sacerdoti... Bug fixed: a symbol must be formed of just one (unicode...
2005-06-07 Enrico Tassiadded syntax for letin
2005-06-07 Enrico Tassichanged match syntax:
2005-06-01 Enrico Tassipaths trough terms implemented with a nice hack :)
2005-06-01 Enrico Tassifixed intro.
2005-05-31 Enrico Tassifixed comments
2005-05-27 Stefano Zacchirolicommented out no longer needed macros Redo, Undo, Abort
2005-05-27 Enrico Tassiremoved debug prerr_endline
2005-05-26 Stefano Zacchirolifixed issue with explicit named substitutions
2005-05-25 Stefano Zacchirolibugfix: "match" now works also when no type is provided...
2005-05-25 Enrico Tassi\lambda x.x y ----> \lambda x.(x y)
2005-05-24 Enrico Tassifixed precedence of \to
2005-05-24 Enrico Tassifixed syntax
next