]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 82d4772) | patch
Basic support for interpretations for NG:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 May 2009 08:49:30 +0000 (08:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 May 2009 08:49:30 +0000 (08:49 +0000)
commit5149063488e3771fb55c198e0ecef5fb5aaaab67
tree34bdb163a08c73532178fb76497ce13a5f6bf603tree | snapshot
parent82d4772ee9ac860f0a99b774612d2cf19838bb4bcommit | diff
Basic support for interpretations for NG:
 1) only interpretations for old objects are used
    (i.e. no way yet to declare a new interpretation on a new object)
 2) only interpretations for constants (no inductive definitions/constructors)
    since we have no faithful embedding of new references into old URIs
 3) no support for backtracking (I think)
helm/software/components/acic_content/termAcicContent.ml diff | blob | history
helm/software/components/acic_content/termAcicContent.mli diff | blob | history
helm/software/components/ng_cic_content/.depend diff | blob | history
helm/software/components/ng_cic_content/.depend.opt diff | blob | history
helm/software/components/ng_cic_content/Makefile diff | blob | history
helm/software/components/ng_cic_content/nTermCicContent.ml diff | blob | history
helm/software/components/ng_cic_content/ncic2astMatcher.ml [new file with mode: 0644] blob
helm/software/components/ng_cic_content/ncic2astMatcher.mli [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.