]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 448d932) | patch
- parser improved: constant uris and variable uris are now handled differently
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Oct 2002 10:51:14 +0000 (10:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 28 Oct 2002 10:51:14 +0000 (10:51 +0000)
commit5b6965fc326021ec30894846113665d1b01fe8ee
tree15a92ed9c40abf24825068f5fc16a56b3e8be9a0tree | snapshot
parent448d93205b37c75e7a652edbd40b4857b840f9e4commit | diff
- parser improved: constant uris and variable uris are now handled differently
- the callback function must now return a URI and no more a term
- explicit named substitutions (with syntax { V1 := t1 ; ... ; V2 := t2})
  implemented
helm/ocaml/cic_textual_parser/cicTextualLexer.mll diff | blob | history
helm/ocaml/cic_textual_parser/cicTextualParser.mly diff | blob | history
helm/ocaml/cic_textual_parser/cicTextualParser0.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.