diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-10 12:05:05 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-10 12:05:05 +0000 |
| commit | 264af456f928ee4e329b07449fec6846f78e0d93 (patch) | |
| tree | 0c2a369bd369134d60e2e12c7b169b72f89031ef /contrib/funind/rawtermops.ml | |
| parent | 79fa2898ba31a2bfa484f3e9ac693ff714365758 (diff) | |
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous and current version work).
Changed the type of typing constraints so as to have all the necessary information on abstract tycons.
Updates of subtac to use the new type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/rawtermops.ml')
0 files changed, 0 insertions, 0 deletions