]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ff4c22) | patch
Refine can now also raise Uncertain. The exception is raised every
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Dec 2002 21:07:55 +0000 (21:07 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 23 Dec 2002 21:07:55 +0000 (21:07 +0000)
commit1641d372cb167eb85984d5491f076727bea3d6ea
tree410fab925afcff02fd9462b40a0aa440fe089e10tree | snapshot
parent3ff4c222cac1ed86d6dfc0c622f0cb19c270631dcommit | diff
Refine can now also raise Uncertain. The exception is raised every
time a metavariab le could be instantiated in such a way that the
term could become well-typed. Useful for ambiguous parsing.
helm/ocaml/cic_unification/cicRefine.ml diff | blob | history
helm/ocaml/cic_unification/cicRefine.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.